Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

This file is deprecated, for a tree on list, use Mergesort.v.

A development of Treesort on Heap trees. It has an average complexity of O(n.log n) but of O(n²) in the worst case (e.g. if the list is already sorted)

(* G. Huet 1-9-95 uses Multiset *)

Require Import List Multiset PermutSetoid Relations Sorting.

Section defs.

Trees and heap trees

Definition of trees over an ordered set

  Variable A : Type.
  Variable leA : relation A.
  Variable eqA : relation A.

  Let gtA (x y:A) := ~ leA x y.

  Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
  Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
  Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
  Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
  Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.

  Hint Resolve leA_refl : core.
  Hint Immediate eqA_dec leA_dec leA_antisym : core.

  Let emptyBag := EmptyBag A.
  Let singletonBag := SingletonBag _ eqA_dec.

  Inductive Tree :=
    | Tree_Leaf : Tree
    | Tree_Node : A -> Tree -> Tree -> Tree.

a is lower than a Tree T if T is a Leaf or T is a Node holding b>a

  Definition leA_Tree (a:A) (t:Tree) :=
    match t with
      | Tree_Leaf => True
      | Tree_Node b T1 T2 => leA a b
    end.

  Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall a : A, leA_Tree a Tree_Leaf
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall a : A, leA_Tree a Tree_Leaf
    simpl; auto with datatypes.
  Qed.

  Lemma leA_Tree_Node :
    forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a b : A) (G D : Tree),
leA a b -> leA_Tree a (Tree_Node b G D)
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a b : A) (G D : Tree),
leA a b -> leA_Tree a (Tree_Node b G D)
    simpl; auto with datatypes.
  Qed.

The heap property

  Inductive is_heap : Tree -> Prop :=
    | nil_is_heap : is_heap Tree_Leaf
    | node_is_heap :
      forall (a:A) (T1 T2:Tree),
        leA_Tree a T1 ->
        leA_Tree a T2 ->
        is_heap T1 -> is_heap T2 -> is_heap (Tree_Node a T1 T2).

  Lemma invert_heap :
    forall (a:A) (T1 T2:Tree),
      is_heap (Tree_Node a T1 T2) ->
      leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a : A) (T1 T2 : Tree),
is_heap (Tree_Node a T1 T2) ->
leA_Tree a T1 /\
leA_Tree a T2 /\ is_heap T1 /\ is_heap T2
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (a : A) (T1 T2 : Tree),
is_heap (Tree_Node a T1 T2) ->
leA_Tree a T1 /\
leA_Tree a T2 /\ is_heap T1 /\ is_heap T2
    intros; inversion H; auto with datatypes.
  Qed.

  (* This lemma ought to be generated automatically by the Inversion tools *)
  Lemma is_heap_rect :
    forall P:Tree -> Type,
      P Tree_Leaf ->
      (forall (a:A) (T1 T2:Tree),
	leA_Tree a T1 ->
	leA_Tree a T2 ->
	is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
      forall T:Tree, is_heap T -> P T.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall P : Tree -> Type,
P Tree_Leaf ->
(forall (a : A) (T1 T2 : Tree),
 leA_Tree a T1 ->
 leA_Tree a T2 ->
 is_heap T1 ->
 P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
forall T : Tree, is_heap T -> P T
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall P : Tree -> Type,
P Tree_Leaf ->
(forall (a : A) (T1 T2 : Tree),
 leA_Tree a T1 ->
 leA_Tree a T2 ->
 is_heap T1 ->
 P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
forall T : Tree, is_heap T -> P T
    simple induction T; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
P:Tree -> Type
X:P Tree_Leaf
X0:forall (a : A) (T1 T2 : Tree),
leA_Tree a T1 ->
leA_Tree a T2 ->
is_heap T1 ->
P T1 ->
is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)
T:Tree
forall (a : A) (t : Tree),
(is_heap t -> P t) ->
forall t0 : Tree,
(is_heap t0 -> P t0) ->
is_heap (Tree_Node a t t0) -> P (Tree_Node a t t0)
    intros a G PG D PD PN.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
P:Tree -> Type
X:P Tree_Leaf
X0:forall (a0 : A) (T1 T2 : Tree),
leA_Tree a0 T1 ->
leA_Tree a0 T2 ->
is_heap T1 ->
P T1 ->
is_heap T2 -> P T2 -> P (Tree_Node a0 T1 T2)
T:Tree
a:A
G:Tree
PG:is_heap G -> P G
D:Tree
PD:is_heap D -> P D
PN:is_heap (Tree_Node a G D)
P (Tree_Node a G D)
    elim (invert_heap a G D); auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
P:Tree -> Type
X:P Tree_Leaf
X0:forall (a0 : A) (T1 T2 : Tree),
leA_Tree a0 T1 ->
leA_Tree a0 T2 ->
is_heap T1 ->
P T1 ->
is_heap T2 -> P T2 -> P (Tree_Node a0 T1 T2)
T:Tree
a:A
G:Tree
PG:is_heap G -> P G
D:Tree
PD:is_heap D -> P D
PN:is_heap (Tree_Node a G D)
leA_Tree a G ->
leA_Tree a D /\ is_heap G /\ is_heap D ->
P (Tree_Node a G D)
    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
P:Tree -> Type
X:P Tree_Leaf
X0:forall (a0 : A) (T1 T2 : Tree),
leA_Tree a0 T1 ->
leA_Tree a0 T2 ->
is_heap T1 ->
P T1 ->
is_heap T2 -> P T2 -> P (Tree_Node a0 T1 T2)
T:Tree
a:A
G:Tree
PG:is_heap G -> P G
D:Tree
PD:is_heap D -> P D
PN:is_heap (Tree_Node a G D)
H1:leA_Tree a G
H2:leA_Tree a D /\ is_heap G /\ is_heap D
H3:leA_Tree a D
H4:is_heap G /\ is_heap D
H:is_heap G
H0:is_heap D
P (Tree_Node a G D)
    apply X0; auto with datatypes.
  Qed.

  (* This lemma ought to be generated automatically by the Inversion tools *)
  Lemma is_heap_rec :
    forall P:Tree -> Set,
      P Tree_Leaf ->
      (forall (a:A) (T1 T2:Tree),
	leA_Tree a T1 ->
	leA_Tree a T2 ->
	is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
      forall T:Tree, is_heap T -> P T.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall P : Tree -> Set,
P Tree_Leaf ->
(forall (a : A) (T1 T2 : Tree),
 leA_Tree a T1 ->
 leA_Tree a T2 ->
 is_heap T1 ->
 P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
forall T : Tree, is_heap T -> P T
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall P : Tree -> Set,
P Tree_Leaf ->
(forall (a : A) (T1 T2 : Tree),
 leA_Tree a T1 ->
 leA_Tree a T2 ->
 is_heap T1 ->
 P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
forall T : Tree, is_heap T -> P T
    simple induction T; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
P:Tree -> Set
H:P Tree_Leaf
X:forall (a : A) (T1 T2 : Tree),
leA_Tree a T1 ->
leA_Tree a T2 ->
is_heap T1 ->
P T1 ->
is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)
T:Tree
forall (a : A) (t : Tree),
(is_heap t -> P t) ->
forall t0 : Tree,
(is_heap t0 -> P t0) ->
is_heap (Tree_Node a t t0) -> P (Tree_Node a t t0)
    intros a G PG D PD PN.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
P:Tree -> Set
H:P Tree_Leaf
X:forall (a0 : A) (T1 T2 : Tree),
leA_Tree a0 T1 ->
leA_Tree a0 T2 ->
is_heap T1 ->
P T1 ->
is_heap T2 -> P T2 -> P (Tree_Node a0 T1 T2)
T:Tree
a:A
G:Tree
PG:is_heap G -> P G
D:Tree
PD:is_heap D -> P D
PN:is_heap (Tree_Node a G D)
P (Tree_Node a G D)
    elim (invert_heap a G D); auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
P:Tree -> Set
H:P Tree_Leaf
X:forall (a0 : A) (T1 T2 : Tree),
leA_Tree a0 T1 ->
leA_Tree a0 T2 ->
is_heap T1 ->
P T1 ->
is_heap T2 -> P T2 -> P (Tree_Node a0 T1 T2)
T:Tree
a:A
G:Tree
PG:is_heap G -> P G
D:Tree
PD:is_heap D -> P D
PN:is_heap (Tree_Node a G D)
leA_Tree a G ->
leA_Tree a D /\ is_heap G /\ is_heap D ->
P (Tree_Node a G D)
    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
P:Tree -> Set
H:P Tree_Leaf
X:forall (a0 : A) (T1 T2 : Tree),
leA_Tree a0 T1 ->
leA_Tree a0 T2 ->
is_heap T1 ->
P T1 ->
is_heap T2 -> P T2 -> P (Tree_Node a0 T1 T2)
T:Tree
a:A
G:Tree
PG:is_heap G -> P G
D:Tree
PD:is_heap D -> P D
PN:is_heap (Tree_Node a G D)
H1:leA_Tree a G
H2:leA_Tree a D /\ is_heap G /\ is_heap D
H3:leA_Tree a D
H4:is_heap G /\ is_heap D
H0:is_heap G
H5:is_heap D
P (Tree_Node a G D)
    apply X; auto with datatypes.
  Qed.

  Lemma low_trans :
    forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (T : Tree) (a b : A),
leA a b -> leA_Tree b T -> leA_Tree a T
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall (T : Tree) (a b : A),
leA a b -> leA_Tree b T -> leA_Tree a T
    simple induction T; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
forall (a : A) (t : Tree),
(forall a0 b : A,
 leA a0 b -> leA_Tree b t -> leA_Tree a0 t) ->
forall t0 : Tree,
(forall a0 b : A,
 leA a0 b -> leA_Tree b t0 -> leA_Tree a0 t0) ->
forall a0 b : A,
leA a0 b ->
leA_Tree b (Tree_Node a t t0) ->
leA_Tree a0 (Tree_Node a t t0)
    intros; simpl; apply leA_trans with b; auto with datatypes.
  Qed.

Merging two sorted lists

   Inductive merge_lem (l1 l2:list A) : Type :=
    merge_exist :
    forall l:list A,
      Sorted leA l ->
      meq (list_contents _ eqA_dec l)
      (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->
      (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) ->
      merge_lem l1 l2.
  Import Morphisms.
  
  Instance: Equivalence (@meq A).A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
Equivalence (meq (A:=A))
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
Equivalence (meq (A:=A)) constructor; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
Transitive (meq (A:=A)) red.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall x y z : multiset A,
meq x y -> meq y z -> meq x z apply meq_trans. Defined.

  Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
Proper (meq (A:=A) ==> meq (A:=A) ==> meq (A:=A))
  (munion (A:=A))
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
Proper (meq (A:=A) ==> meq (A:=A) ==> meq (A:=A))
  (munion (A:=A)) intros x y H x' y' H'.A:Type
leA, eqA:relation A
gtA:=fun x0 y0 : A => ~ leA x0 y0:A -> A -> Prop
leA_dec:forall x0 y0 : A, {leA x0 y0} + {leA y0 x0}
eqA_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
leA_refl:forall x0 y0 : A, eqA x0 y0 -> leA x0 y0
leA_trans:forall x0 y0 z : A,
leA x0 y0 -> leA y0 z -> leA x0 z
leA_antisym:forall x0 y0 : A,
leA x0 y0 -> leA y0 x0 -> eqA x0 y0
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
x, y:multiset A
H:meq x y
x', y':multiset A
H':meq x' y'
meq (munion x x') (munion y y') now apply meq_congr. Qed.
  
  Lemma merge :
    forall l1:list A, Sorted leA l1 ->
    forall l2:list A, Sorted leA l2 -> merge_lem l1 l2.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A, Sorted leA l2 -> merge_lem l1 l2
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A, Sorted leA l2 -> merge_lem l1 l2
    fix merge 1; intros; destruct l1.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l0 : list A,
Sorted leA l0 -> merge_lem l1 l0
H:Sorted leA nil
l2:list A
H0:Sorted leA l2
merge_lem nil l2
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l0 : list A,
Sorted leA l0 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l0 l3
a:A
l1:list A
H:Sorted leA (a :: l1)
l2:list A
H0:Sorted leA l2
merge_lem (a :: l1) l2
    apply merge_exist with l2; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l0 : list A,
Sorted leA l0 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l0 l3
a:A
l1:list A
H:Sorted leA (a :: l1)
l2:list A
H0:Sorted leA l2
merge_lem (a :: l1) l2
    rename l1 into l.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l0 : list A,
Sorted leA l0 -> merge_lem l1 l0
a:A
l:list A
H:Sorted leA (a :: l)
l2:list A
H0:Sorted leA l2
merge_lem (a :: l) l2
    revert l2 H0.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2 fix merge0 1.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2 intros.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l0 : list A,
Sorted leA l0 -> merge_lem l1 l0
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l0 : list A,
Sorted leA l0 -> merge_lem (a :: l) l0
l2:list A
H0:Sorted leA l2
merge_lem (a :: l) l2
    destruct l2 as [|a0 l0].A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
H0:Sorted leA nil
merge_lem (a :: l) nil
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
merge_lem (a :: l) (a0 :: l0) 
    apply merge_exist with (a :: l); simpl; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
merge_lem (a :: l) (a0 :: l0) 
    induction (leA_dec a a0) as [Hle|Hle].A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
merge_lem (a :: l) (a0 :: l0)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0)

    (* 1 (leA a a0) *)
    apply Sorted_inv in H.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA l /\ HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
merge_lem (a :: l) (a0 :: l0)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0) destruct H.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
merge_lem (a :: l) (a0 :: l0)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0)
    destruct (merge l H (a0 :: l0) H0) as [l1 H2 H3 H4].A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
merge_lem (a :: l) (a0 :: l0)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0)
    apply merge_exist with (a :: l1).A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
Sorted leA (a :: l1)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
meq (list_contents eqA eqA_dec (a :: l1))
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec (a0 :: l0)))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a :: l1)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0) clear merge merge0.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
Sorted leA (a :: l1)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
meq (list_contents eqA eqA_dec (a :: l1))
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec (a0 :: l0)))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a :: l1)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0)
      auto using cons_sort, cons_leA with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
meq (list_contents eqA eqA_dec (a :: l1))
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec (a0 :: l0)))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a :: l1)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0)
    simpl.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
meq
  (munion (SingletonBag eqA eqA_dec a)
     (list_contents eqA eqA_dec l1))
  (munion
     (munion (SingletonBag eqA eqA_dec a)
        (list_contents eqA eqA_dec l))
     (munion (SingletonBag eqA eqA_dec a0)
        (list_contents eqA eqA_dec l0)))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a :: l1)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0) rewrite H3.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
meq
  (munion (SingletonBag eqA eqA_dec a)
     (munion (list_contents eqA eqA_dec l)
        (list_contents eqA eqA_dec (a0 :: l0))))
  (munion
     (munion (SingletonBag eqA eqA_dec a)
        (list_contents eqA eqA_dec l))
     (munion (SingletonBag eqA eqA_dec a0)
        (list_contents eqA eqA_dec l0)))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a :: l1)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0) now rewrite munion_ass.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a1 : A,
HdRel leA a1 l ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a :: l1)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0)
    intros.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a2 : A,
HdRel leA a2 l ->
HdRel leA a2 (a0 :: l0) -> HdRel leA a2 l1
a1:A
H5:HdRel leA a1 (a :: l)
H6:HdRel leA a1 (a0 :: l0)
HdRel leA a1 (a :: l1)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0) apply cons_leA.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA l
H1:HdRel leA a l
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a a0
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec l)
     (list_contents eqA eqA_dec (a0 :: l0)))
H4:forall a2 : A,
HdRel leA a2 l ->
HdRel leA a2 (a0 :: l0) -> HdRel leA a2 l1
a1:A
H5:HdRel leA a1 (a :: l)
H6:HdRel leA a1 (a0 :: l0)
leA a1 a
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0) 
    apply (@HdRel_inv _ leA) with l; trivial with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA (a0 :: l0)
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0)

    (* 2 (leA a0 a) *)
    apply Sorted_inv in H0.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA l0 /\ HdRel leA a0 l0
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0) destruct H0.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l1 : list A,
Sorted leA l1 ->
forall l2 : list A,
Sorted leA l2 -> merge_lem l1 l2
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
merge_lem (a :: l) (a0 :: l0)
    destruct (merge0 l0 H0) as [l1 H2 H3 H4].A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
merge:forall l2 : list A,
Sorted leA l2 ->
forall l3 : list A,
Sorted leA l3 -> merge_lem l2 l3
a:A
l:list A
H:Sorted leA (a :: l)
merge0:forall l2 : list A,
Sorted leA l2 -> merge_lem (a :: l) l2
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
merge_lem (a :: l) (a0 :: l0) clear merge merge0.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
merge_lem (a :: l) (a0 :: l0)  
    apply merge_exist with (a0 :: l1); 
      auto using cons_sort, cons_leA with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
meq (list_contents eqA eqA_dec (a0 :: l1))
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec (a0 :: l0)))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a0 :: l1)
    simpl; rewrite H3.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
meq
  (munion (SingletonBag eqA eqA_dec a0)
     (munion (list_contents eqA eqA_dec (a :: l))
        (list_contents eqA eqA_dec l0)))
  (munion
     (munion (SingletonBag eqA eqA_dec a)
        (list_contents eqA eqA_dec l))
     (munion (SingletonBag eqA eqA_dec a0)
        (list_contents eqA eqA_dec l0)))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a0 :: l1) simpl.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
meq
  (munion (SingletonBag eqA eqA_dec a0)
     (munion
        (munion (SingletonBag eqA eqA_dec a)
           (list_contents eqA eqA_dec l))
        (list_contents eqA eqA_dec l0)))
  (munion
     (munion (SingletonBag eqA eqA_dec a)
        (list_contents eqA eqA_dec l))
     (munion (SingletonBag eqA eqA_dec a0)
        (list_contents eqA eqA_dec l0)))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a0 :: l1) setoid_rewrite munion_ass at 1.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
meq
  (munion (SingletonBag eqA eqA_dec a0)
     (munion (SingletonBag eqA eqA_dec a)
        (munion (list_contents eqA eqA_dec l)
           (list_contents eqA eqA_dec l0))))
  (munion
     (munion (SingletonBag eqA eqA_dec a)
        (list_contents eqA eqA_dec l))
     (munion (SingletonBag eqA eqA_dec a0)
        (list_contents eqA eqA_dec l0)))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a0 :: l1) rewrite munion_comm.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
meq
  (munion
     (munion (SingletonBag eqA eqA_dec a)
        (munion (list_contents eqA eqA_dec l)
           (list_contents eqA eqA_dec l0)))
     (SingletonBag eqA eqA_dec a0))
  (munion
     (munion (SingletonBag eqA eqA_dec a)
        (list_contents eqA eqA_dec l))
     (munion (SingletonBag eqA eqA_dec a0)
        (list_contents eqA eqA_dec l0)))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a0 :: l1)
    repeat rewrite munion_ass.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
meq
  (munion (SingletonBag eqA eqA_dec a)
     (munion (list_contents eqA eqA_dec l)
        (munion (list_contents eqA eqA_dec l0)
           (SingletonBag eqA eqA_dec a0))))
  (munion (SingletonBag eqA eqA_dec a)
     (munion (list_contents eqA eqA_dec l)
        (munion (SingletonBag eqA eqA_dec a0)
           (list_contents eqA eqA_dec l0))))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a0 :: l1) setoid_rewrite munion_comm at 3.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
meq
  (munion (SingletonBag eqA eqA_dec a)
     (munion (list_contents eqA eqA_dec l)
        (munion (SingletonBag eqA eqA_dec a0)
           (list_contents eqA eqA_dec l0))))
  (munion (SingletonBag eqA eqA_dec a)
     (munion (list_contents eqA eqA_dec l)
        (munion (SingletonBag eqA eqA_dec a0)
           (list_contents eqA eqA_dec l0))))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a0 :: l1) reflexivity.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 l0 -> HdRel leA a1 l1
forall a1 : A,
HdRel leA a1 (a :: l) ->
HdRel leA a1 (a0 :: l0) -> HdRel leA a1 (a0 :: l1)
    intros.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a2 : A,
HdRel leA a2 (a :: l) ->
HdRel leA a2 l0 -> HdRel leA a2 l1
a1:A
H5:HdRel leA a1 (a :: l)
H6:HdRel leA a1 (a0 :: l0)
HdRel leA a1 (a0 :: l1) apply cons_leA.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
a:A
l:list A
H:Sorted leA (a :: l)
a0:A
l0:list A
H0:Sorted leA l0
H1:HdRel leA a0 l0
Hle:leA a0 a
l1:list A
H2:Sorted leA l1
H3:meq (list_contents eqA eqA_dec l1)
  (munion (list_contents eqA eqA_dec (a :: l))
     (list_contents eqA eqA_dec l0))
H4:forall a2 : A,
HdRel leA a2 (a :: l) ->
HdRel leA a2 l0 -> HdRel leA a2 l1
a1:A
H5:HdRel leA a1 (a :: l)
H6:HdRel leA a1 (a0 :: l0)
leA a1 a0 
    apply (@HdRel_inv _ leA) with l0; trivial with datatypes.
  Qed.

From trees to multisets

contents of a tree as a multiset

Nota Bene : In what follows the definition of SingletonBag in not used. Actually, we could just take as postulate: Parameter SingletonBag : A→multiset.

  Fixpoint contents (t:Tree) : multiset A :=
    match t with
      | Tree_Leaf => emptyBag
      | Tree_Node a t1 t2 =>
	munion (contents t1) (munion (contents t2) (singletonBag a))
    end.

equivalence of two trees is equality of corresponding multisets

  Definition equiv_Tree (t1 t2:Tree) := meq (contents t1) (contents t2).

From lists to sorted lists

Specification of heap insertion

  Inductive insert_spec (a:A) (T:Tree) : Type :=
    insert_exist :
    forall T1:Tree,
      is_heap T1 ->
      meq (contents T1) (munion (contents T) (singletonBag a)) ->
      (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
      insert_spec a T.


  Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall T : Tree,
is_heap T -> forall a : A, insert_spec a T
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall T : Tree,
is_heap T -> forall a : A, insert_spec a T
    simple induction 1; intros.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
insert_spec a Tree_Leaf
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
insert_spec a0 (Tree_Node a T1 T2)
    apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
insert_spec a0 (Tree_Node a T1 T2)
    simpl; unfold meq, munion; auto using node_is_heap with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
insert_spec a0 (Tree_Node a T1 T2)
    elim (leA_dec a a0); intros.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a2 : A, insert_spec a2 T1
H3:is_heap T2
X0:forall a2 : A, insert_spec a2 T2
a0:A
a1:leA a a0
insert_spec a0 (Tree_Node a T1 T2)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
insert_spec a0 (Tree_Node a T1 T2)
    elim (X a0); intros.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a2 : A, insert_spec a2 T1
H3:is_heap T2
X0:forall a2 : A, insert_spec a2 T2
a0:A
a1:leA a a0
T0:Tree
i:is_heap T0
m:meq (contents T0)
  (munion (contents T1) (singletonBag a0))
l:forall b : A,
leA b a0 -> leA_Tree b T1 -> leA_Tree b T0
insert_spec a0 (Tree_Node a T1 T2)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
insert_spec a0 (Tree_Node a T1 T2)
    apply insert_exist with (Tree_Node a T2 T0);
      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a2 : A, insert_spec a2 T1
H3:is_heap T2
X0:forall a2 : A, insert_spec a2 T2
a0:A
a1:leA a a0
T0:Tree
i:is_heap T0
m:meq (contents T0)
  (munion (contents T1) (singletonBag a0))
l:forall b : A,
leA b a0 -> leA_Tree b T1 -> leA_Tree b T0
meq (contents (Tree_Node a T2 T0))
  (munion (contents (Tree_Node a T1 T2))
     (singletonBag a0))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
insert_spec a0 (Tree_Node a T1 T2)
    simpl; apply treesort_twist1; trivial with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
insert_spec a0 (Tree_Node a T1 T2)
    elim (X a); intros T3 HeapT3 ConT3 LeA.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
T3:Tree
HeapT3:is_heap T3
ConT3:meq (contents T3)
  (munion (contents T1) (singletonBag a))
LeA:forall b0 : A,
leA b0 a -> leA_Tree b0 T1 -> leA_Tree b0 T3
insert_spec a0 (Tree_Node a T1 T2)
    apply insert_exist with (Tree_Node a0 T2 T3);
      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
T3:Tree
HeapT3:is_heap T3
ConT3:meq (contents T3)
  (munion (contents T1) (singletonBag a))
LeA:forall b0 : A,
leA b0 a -> leA_Tree b0 T1 -> leA_Tree b0 T3
is_heap (Tree_Node a0 T2 T3)
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
T3:Tree
HeapT3:is_heap T3
ConT3:meq (contents T3)
  (munion (contents T1) (singletonBag a))
LeA:forall b0 : A,
leA b0 a -> leA_Tree b0 T1 -> leA_Tree b0 T3
meq (contents (Tree_Node a0 T2 T3))
  (munion (contents (Tree_Node a T1 T2))
     (singletonBag a0))
    apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
T3:Tree
HeapT3:is_heap T3
ConT3:meq (contents T3)
  (munion (contents T1) (singletonBag a))
LeA:forall b0 : A,
leA b0 a -> leA_Tree b0 T1 -> leA_Tree b0 T3
leA_Tree a0 T2
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
T3:Tree
HeapT3:is_heap T3
ConT3:meq (contents T3)
  (munion (contents T1) (singletonBag a))
LeA:forall b0 : A,
leA b0 a -> leA_Tree b0 T1 -> leA_Tree b0 T3
leA_Tree a0 T3
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
T3:Tree
HeapT3:is_heap T3
ConT3:meq (contents T3)
  (munion (contents T1) (singletonBag a))
LeA:forall b0 : A,
leA b0 a -> leA_Tree b0 T1 -> leA_Tree b0 T3
meq (contents (Tree_Node a0 T2 T3))
  (munion (contents (Tree_Node a T1 T2))
     (singletonBag a0))
    apply low_trans with a; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
T3:Tree
HeapT3:is_heap T3
ConT3:meq (contents T3)
  (munion (contents T1) (singletonBag a))
LeA:forall b0 : A,
leA b0 a -> leA_Tree b0 T1 -> leA_Tree b0 T3
leA_Tree a0 T3
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
T3:Tree
HeapT3:is_heap T3
ConT3:meq (contents T3)
  (munion (contents T1) (singletonBag a))
LeA:forall b0 : A,
leA b0 a -> leA_Tree b0 T1 -> leA_Tree b0 T3
meq (contents (Tree_Node a0 T2 T3))
  (munion (contents (Tree_Node a T1 T2))
     (singletonBag a0))
    apply LeA; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
T3:Tree
HeapT3:is_heap T3
ConT3:meq (contents T3)
  (munion (contents T1) (singletonBag a))
LeA:forall b0 : A,
leA b0 a -> leA_Tree b0 T1 -> leA_Tree b0 T3
leA_Tree a0 T1
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
T3:Tree
HeapT3:is_heap T3
ConT3:meq (contents T3)
  (munion (contents T1) (singletonBag a))
LeA:forall b0 : A,
leA b0 a -> leA_Tree b0 T1 -> leA_Tree b0 T3
meq (contents (Tree_Node a0 T2 T3))
  (munion (contents (Tree_Node a T1 T2))
     (singletonBag a0))
    apply low_trans with a; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
H:is_heap T
a:A
T1, T2:Tree
H0:leA_Tree a T1
H1:leA_Tree a T2
H2:is_heap T1
X:forall a1 : A, insert_spec a1 T1
H3:is_heap T2
X0:forall a1 : A, insert_spec a1 T2
a0:A
b:leA a0 a
T3:Tree
HeapT3:is_heap T3
ConT3:meq (contents T3)
  (munion (contents T1) (singletonBag a))
LeA:forall b0 : A,
leA b0 a -> leA_Tree b0 T1 -> leA_Tree b0 T3
meq (contents (Tree_Node a0 T2 T3))
  (munion (contents (Tree_Node a T1 T2))
     (singletonBag a0))
    simpl; apply treesort_twist2; trivial with datatypes.
  Qed.

Building a heap from a list

  Inductive build_heap (l:list A) : Type :=
    heap_exist :
    forall T:Tree,
      is_heap T ->
      meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.

  Lemma list_to_heap : forall l:list A, build_heap l.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l : list A, build_heap l
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l : list A, build_heap l
    simple induction l.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
build_heap nil
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
forall (a : A) (l0 : list A),
build_heap l0 -> build_heap (a :: l0)
    apply (heap_exist nil Tree_Leaf); auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
is_heap Tree_Leaf
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
forall (a : A) (l0 : list A),
build_heap l0 -> build_heap (a :: l0)
    simpl; unfold meq; exact nil_is_heap.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
forall (a : A) (l0 : list A),
build_heap l0 -> build_heap (a :: l0)
    simple induction 1.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
l0:list A
X:build_heap l0
forall T : Tree,
is_heap T ->
meq (list_contents eqA eqA_dec l0) (contents T) ->
build_heap (a :: l0)
    intros T i m; elim (insert T i a).A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
l0:list A
X:build_heap l0
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l0) (contents T)
forall T1 : Tree,
is_heap T1 ->
meq (contents T1)
  (munion (contents T) (singletonBag a)) ->
(forall b : A,
 leA b a -> leA_Tree b T -> leA_Tree b T1) ->
build_heap (a :: l0)
    intros; apply heap_exist with T1; simpl; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
l0:list A
X:build_heap l0
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l0) (contents T)
T1:Tree
i0:is_heap T1
m0:meq (contents T1)
  (munion (contents T) (singletonBag a))
l1:forall b : A,
leA b a -> leA_Tree b T -> leA_Tree b T1
meq
  (munion (SingletonBag eqA eqA_dec a)
     (list_contents eqA eqA_dec l0)) (contents T1)
    apply meq_trans with (munion (contents T) (singletonBag a)).A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
l0:list A
X:build_heap l0
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l0) (contents T)
T1:Tree
i0:is_heap T1
m0:meq (contents T1)
  (munion (contents T) (singletonBag a))
l1:forall b : A,
leA b a -> leA_Tree b T -> leA_Tree b T1
meq
  (munion (SingletonBag eqA eqA_dec a)
     (list_contents eqA eqA_dec l0))
  (munion (contents T) (singletonBag a))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
l0:list A
X:build_heap l0
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l0) (contents T)
T1:Tree
i0:is_heap T1
m0:meq (contents T1)
  (munion (contents T) (singletonBag a))
l1:forall b : A,
leA b a -> leA_Tree b T -> leA_Tree b T1
meq (munion (contents T) (singletonBag a))
  (contents T1)
    apply meq_trans with (munion (singletonBag a) (contents T)).A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
l0:list A
X:build_heap l0
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l0) (contents T)
T1:Tree
i0:is_heap T1
m0:meq (contents T1)
  (munion (contents T) (singletonBag a))
l1:forall b : A,
leA b a -> leA_Tree b T -> leA_Tree b T1
meq
  (munion (SingletonBag eqA eqA_dec a)
     (list_contents eqA eqA_dec l0))
  (munion (singletonBag a) (contents T))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
l0:list A
X:build_heap l0
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l0) (contents T)
T1:Tree
i0:is_heap T1
m0:meq (contents T1)
  (munion (contents T) (singletonBag a))
l1:forall b : A,
leA b a -> leA_Tree b T -> leA_Tree b T1
meq (munion (singletonBag a) (contents T))
  (munion (contents T) (singletonBag a))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
l0:list A
X:build_heap l0
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l0) (contents T)
T1:Tree
i0:is_heap T1
m0:meq (contents T1)
  (munion (contents T) (singletonBag a))
l1:forall b : A,
leA b a -> leA_Tree b T -> leA_Tree b T1
meq (munion (contents T) (singletonBag a))
  (contents T1)
    apply meq_right; trivial with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
l0:list A
X:build_heap l0
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l0) (contents T)
T1:Tree
i0:is_heap T1
m0:meq (contents T1)
  (munion (contents T) (singletonBag a))
l1:forall b : A,
leA b a -> leA_Tree b T -> leA_Tree b T1
meq (munion (singletonBag a) (contents T))
  (munion (contents T) (singletonBag a))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
l0:list A
X:build_heap l0
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l0) (contents T)
T1:Tree
i0:is_heap T1
m0:meq (contents T1)
  (munion (contents T) (singletonBag a))
l1:forall b : A,
leA b a -> leA_Tree b T -> leA_Tree b T1
meq (munion (contents T) (singletonBag a))
  (contents T1)
    apply munion_comm.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
a:A
l0:list A
X:build_heap l0
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l0) (contents T)
T1:Tree
i0:is_heap T1
m0:meq (contents T1)
  (munion (contents T) (singletonBag a))
l1:forall b : A,
leA b a -> leA_Tree b T -> leA_Tree b T1
meq (munion (contents T) (singletonBag a))
  (contents T1)
    apply meq_sym; trivial with datatypes.
  Qed.

Building the sorted list

  Inductive flat_spec (T:Tree) : Type :=
    flat_exist :
    forall l:list A,
      Sorted leA l ->
      (forall a:A, leA_Tree a T -> HdRel leA a l) ->
      meq (contents T) (list_contents _ eqA_dec l) -> flat_spec T.

  Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall T : Tree, is_heap T -> flat_spec T
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall T : Tree, is_heap T -> flat_spec T
    intros T h; elim h; intros.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
h:is_heap T
flat_spec Tree_Leaf
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
h:is_heap T
a:A
T1, T2:Tree
H:leA_Tree a T1
H0:leA_Tree a T2
H1:is_heap T1
X:flat_spec T1
H2:is_heap T2
X0:flat_spec T2
flat_spec (Tree_Node a T1 T2)
    apply flat_exist with (nil (A:=A)); auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
h:is_heap T
a:A
T1, T2:Tree
H:leA_Tree a T1
H0:leA_Tree a T2
H1:is_heap T1
X:flat_spec T1
H2:is_heap T2
X0:flat_spec T2
flat_spec (Tree_Node a T1 T2)
    elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
h:is_heap T
a:A
T1, T2:Tree
H:leA_Tree a T1
H0:leA_Tree a T2
H1:is_heap T1
X:flat_spec T1
H2:is_heap T2
X0:flat_spec T2
l1:list A
s1:Sorted leA l1
i1:forall a0 : A, leA_Tree a0 T1 -> HdRel leA a0 l1
m1:meq (contents T1) (list_contents eqA eqA_dec l1)
l2:list A
s2:Sorted leA l2
i2:forall a0 : A, leA_Tree a0 T2 -> HdRel leA a0 l2
m2:meq (contents T2) (list_contents eqA eqA_dec l2)
flat_spec (Tree_Node a T1 T2)
    elim (merge _ s1 _ s2); intros.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
h:is_heap T
a:A
T1, T2:Tree
H:leA_Tree a T1
H0:leA_Tree a T2
H1:is_heap T1
X:flat_spec T1
H2:is_heap T2
X0:flat_spec T2
l1:list A
s1:Sorted leA l1
i1:forall a0 : A, leA_Tree a0 T1 -> HdRel leA a0 l1
m1:meq (contents T1) (list_contents eqA eqA_dec l1)
l2:list A
s2:Sorted leA l2
i2:forall a0 : A, leA_Tree a0 T2 -> HdRel leA a0 l2
m2:meq (contents T2) (list_contents eqA eqA_dec l2)
l:list A
s:Sorted leA l
m:meq (list_contents eqA eqA_dec l)
  (munion (list_contents eqA eqA_dec l1)
     (list_contents eqA eqA_dec l2))
h0:forall a0 : A,
HdRel leA a0 l1 ->
HdRel leA a0 l2 -> HdRel leA a0 l
flat_spec (Tree_Node a T1 T2)
    apply flat_exist with (a :: l); simpl; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
h:is_heap T
a:A
T1, T2:Tree
H:leA_Tree a T1
H0:leA_Tree a T2
H1:is_heap T1
X:flat_spec T1
H2:is_heap T2
X0:flat_spec T2
l1:list A
s1:Sorted leA l1
i1:forall a0 : A, leA_Tree a0 T1 -> HdRel leA a0 l1
m1:meq (contents T1) (list_contents eqA eqA_dec l1)
l2:list A
s2:Sorted leA l2
i2:forall a0 : A, leA_Tree a0 T2 -> HdRel leA a0 l2
m2:meq (contents T2) (list_contents eqA eqA_dec l2)
l:list A
s:Sorted leA l
m:meq (list_contents eqA eqA_dec l)
  (munion (list_contents eqA eqA_dec l1)
     (list_contents eqA eqA_dec l2))
h0:forall a0 : A,
HdRel leA a0 l1 ->
HdRel leA a0 l2 -> HdRel leA a0 l
meq
  (munion (contents T1)
     (munion (contents T2) (singletonBag a)))
  (munion (SingletonBag eqA eqA_dec a)
     (list_contents eqA eqA_dec l))
    apply meq_trans with
      (munion (list_contents _ eqA_dec l1)
	(munion (list_contents _ eqA_dec l2) (singletonBag a))).A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
h:is_heap T
a:A
T1, T2:Tree
H:leA_Tree a T1
H0:leA_Tree a T2
H1:is_heap T1
X:flat_spec T1
H2:is_heap T2
X0:flat_spec T2
l1:list A
s1:Sorted leA l1
i1:forall a0 : A, leA_Tree a0 T1 -> HdRel leA a0 l1
m1:meq (contents T1) (list_contents eqA eqA_dec l1)
l2:list A
s2:Sorted leA l2
i2:forall a0 : A, leA_Tree a0 T2 -> HdRel leA a0 l2
m2:meq (contents T2) (list_contents eqA eqA_dec l2)
l:list A
s:Sorted leA l
m:meq (list_contents eqA eqA_dec l)
  (munion (list_contents eqA eqA_dec l1)
     (list_contents eqA eqA_dec l2))
h0:forall a0 : A,
HdRel leA a0 l1 ->
HdRel leA a0 l2 -> HdRel leA a0 l
meq
  (munion (contents T1)
     (munion (contents T2) (singletonBag a)))
  (munion (list_contents eqA eqA_dec l1)
     (munion (list_contents eqA eqA_dec l2)
        (singletonBag a)))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
h:is_heap T
a:A
T1, T2:Tree
H:leA_Tree a T1
H0:leA_Tree a T2
H1:is_heap T1
X:flat_spec T1
H2:is_heap T2
X0:flat_spec T2
l1:list A
s1:Sorted leA l1
i1:forall a0 : A, leA_Tree a0 T1 -> HdRel leA a0 l1
m1:meq (contents T1) (list_contents eqA eqA_dec l1)
l2:list A
s2:Sorted leA l2
i2:forall a0 : A, leA_Tree a0 T2 -> HdRel leA a0 l2
m2:meq (contents T2) (list_contents eqA eqA_dec l2)
l:list A
s:Sorted leA l
m:meq (list_contents eqA eqA_dec l)
  (munion (list_contents eqA eqA_dec l1)
     (list_contents eqA eqA_dec l2))
h0:forall a0 : A,
HdRel leA a0 l1 ->
HdRel leA a0 l2 -> HdRel leA a0 l
meq
  (munion (list_contents eqA eqA_dec l1)
     (munion (list_contents eqA eqA_dec l2)
        (singletonBag a)))
  (munion (SingletonBag eqA eqA_dec a)
     (list_contents eqA eqA_dec l))
    apply meq_congr; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
h:is_heap T
a:A
T1, T2:Tree
H:leA_Tree a T1
H0:leA_Tree a T2
H1:is_heap T1
X:flat_spec T1
H2:is_heap T2
X0:flat_spec T2
l1:list A
s1:Sorted leA l1
i1:forall a0 : A, leA_Tree a0 T1 -> HdRel leA a0 l1
m1:meq (contents T1) (list_contents eqA eqA_dec l1)
l2:list A
s2:Sorted leA l2
i2:forall a0 : A, leA_Tree a0 T2 -> HdRel leA a0 l2
m2:meq (contents T2) (list_contents eqA eqA_dec l2)
l:list A
s:Sorted leA l
m:meq (list_contents eqA eqA_dec l)
  (munion (list_contents eqA eqA_dec l1)
     (list_contents eqA eqA_dec l2))
h0:forall a0 : A,
HdRel leA a0 l1 ->
HdRel leA a0 l2 -> HdRel leA a0 l
meq
  (munion (list_contents eqA eqA_dec l1)
     (munion (list_contents eqA eqA_dec l2)
        (singletonBag a)))
  (munion (SingletonBag eqA eqA_dec a)
     (list_contents eqA eqA_dec l))
    apply meq_trans with
      (munion (singletonBag a)
	(munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
h:is_heap T
a:A
T1, T2:Tree
H:leA_Tree a T1
H0:leA_Tree a T2
H1:is_heap T1
X:flat_spec T1
H2:is_heap T2
X0:flat_spec T2
l1:list A
s1:Sorted leA l1
i1:forall a0 : A, leA_Tree a0 T1 -> HdRel leA a0 l1
m1:meq (contents T1) (list_contents eqA eqA_dec l1)
l2:list A
s2:Sorted leA l2
i2:forall a0 : A, leA_Tree a0 T2 -> HdRel leA a0 l2
m2:meq (contents T2) (list_contents eqA eqA_dec l2)
l:list A
s:Sorted leA l
m:meq (list_contents eqA eqA_dec l)
  (munion (list_contents eqA eqA_dec l1)
     (list_contents eqA eqA_dec l2))
h0:forall a0 : A,
HdRel leA a0 l1 ->
HdRel leA a0 l2 -> HdRel leA a0 l
meq
  (munion (list_contents eqA eqA_dec l1)
     (munion (list_contents eqA eqA_dec l2)
        (singletonBag a)))
  (munion (singletonBag a)
     (munion (list_contents eqA eqA_dec l1)
        (list_contents eqA eqA_dec l2)))
A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
h:is_heap T
a:A
T1, T2:Tree
H:leA_Tree a T1
H0:leA_Tree a T2
H1:is_heap T1
X:flat_spec T1
H2:is_heap T2
X0:flat_spec T2
l1:list A
s1:Sorted leA l1
i1:forall a0 : A, leA_Tree a0 T1 -> HdRel leA a0 l1
m1:meq (contents T1) (list_contents eqA eqA_dec l1)
l2:list A
s2:Sorted leA l2
i2:forall a0 : A, leA_Tree a0 T2 -> HdRel leA a0 l2
m2:meq (contents T2) (list_contents eqA eqA_dec l2)
l:list A
s:Sorted leA l
m:meq (list_contents eqA eqA_dec l)
  (munion (list_contents eqA eqA_dec l1)
     (list_contents eqA eqA_dec l2))
h0:forall a0 : A,
HdRel leA a0 l1 ->
HdRel leA a0 l2 -> HdRel leA a0 l
meq
  (munion (singletonBag a)
     (munion (list_contents eqA eqA_dec l1)
        (list_contents eqA eqA_dec l2)))
  (munion (SingletonBag eqA eqA_dec a)
     (list_contents eqA eqA_dec l))
    apply munion_rotate.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
T:Tree
h:is_heap T
a:A
T1, T2:Tree
H:leA_Tree a T1
H0:leA_Tree a T2
H1:is_heap T1
X:flat_spec T1
H2:is_heap T2
X0:flat_spec T2
l1:list A
s1:Sorted leA l1
i1:forall a0 : A, leA_Tree a0 T1 -> HdRel leA a0 l1
m1:meq (contents T1) (list_contents eqA eqA_dec l1)
l2:list A
s2:Sorted leA l2
i2:forall a0 : A, leA_Tree a0 T2 -> HdRel leA a0 l2
m2:meq (contents T2) (list_contents eqA eqA_dec l2)
l:list A
s:Sorted leA l
m:meq (list_contents eqA eqA_dec l)
  (munion (list_contents eqA eqA_dec l1)
     (list_contents eqA eqA_dec l2))
h0:forall a0 : A,
HdRel leA a0 l1 ->
HdRel leA a0 l2 -> HdRel leA a0 l
meq
  (munion (singletonBag a)
     (munion (list_contents eqA eqA_dec l1)
        (list_contents eqA eqA_dec l2)))
  (munion (SingletonBag eqA eqA_dec a)
     (list_contents eqA eqA_dec l))
    apply meq_right; apply meq_sym; trivial with datatypes.
  Qed.

Specification of treesort

  Theorem treesort :
    forall l:list A,
    {m : list A | Sorted leA m & permutation _ eqA_dec l m}.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l : list A,
{m : list A | Sorted leA m &
permutation eqA eqA_dec l m}
  Proof.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
forall l : list A,
{m : list A | Sorted leA m &
permutation eqA eqA_dec l m}
    intro l; unfold permutation.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
{m : list A | Sorted leA m &
meq (list_contents eqA eqA_dec l)
  (list_contents eqA eqA_dec m)}
    elim (list_to_heap l).A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
forall T : Tree,
is_heap T ->
meq (list_contents eqA eqA_dec l) (contents T) ->
{m0 : list A | Sorted leA m0 &
meq (list_contents eqA eqA_dec l)
  (list_contents eqA eqA_dec m0)}
    intros.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l) (contents T)
{m0 : list A | Sorted leA m0 &
meq (list_contents eqA eqA_dec l)
  (list_contents eqA eqA_dec m0)}
    elim (heap_to_list T); auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l) (contents T)
forall l0 : list A,
Sorted leA l0 ->
(forall a : A, leA_Tree a T -> HdRel leA a l0) ->
meq (contents T) (list_contents eqA eqA_dec l0) ->
{m1 : list A | Sorted leA m1 &
meq (list_contents eqA eqA_dec l)
  (list_contents eqA eqA_dec m1)}
    intros.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l) (contents T)
l0:list A
s:Sorted leA l0
h:forall a : A, leA_Tree a T -> HdRel leA a l0
m0:meq (contents T) (list_contents eqA eqA_dec l0)
{m1 : list A | Sorted leA m1 &
meq (list_contents eqA eqA_dec l)
  (list_contents eqA eqA_dec m1)}
    exists l0; auto with datatypes.A:Type
leA, eqA:relation A
gtA:=fun x y : A => ~ leA x y:A -> A -> Prop
leA_dec:forall x y : A, {leA x y} + {leA y x}
eqA_dec:forall x y : A, {eqA x y} + {~ eqA x y}
leA_refl:forall x y : A, eqA x y -> leA x y
leA_trans:forall x y z : A,
leA x y -> leA y z -> leA x z
leA_antisym:forall x y : A,
leA x y -> leA y x -> eqA x y
emptyBag:=EmptyBag A:multiset A
singletonBag:=SingletonBag eqA eqA_dec:A -> multiset A
l:list A
T:Tree
i:is_heap T
m:meq (list_contents eqA eqA_dec l) (contents T)
l0:list A
s:Sorted leA l0
h:forall a : A, leA_Tree a T -> HdRel leA a l0
m0:meq (contents T) (list_contents eqA eqA_dec l0)
meq (list_contents eqA eqA_dec l)
  (list_contents eqA eqA_dec l0)
    apply meq_trans with (contents T); trivial with datatypes.
  Qed.

End defs.