diff --git a/samples/Coq/Basics.v b/samples/Coq/Basics.v
deleted file mode 100755
index 054fcbd8..00000000
--- a/samples/Coq/Basics.v
+++ /dev/null
@@ -1,707 +0,0 @@
-Inductive day : Type :=
-| monday : day
-| tuesday : day
-| wednesday : day
-| thursday : day
-| friday : day
-| saturday : day
-| sunday : day.
-
-Definition next_weekday (d:day) : day :=
-  match d with
-  | monday => tuesday
-  | tuesday => wednesday
-  | wednesday => thursday
-  | thursday => friday
-  | friday => monday
-  | saturday => monday
-  | sunday => monday
-  end.
-
-Example test_next_weekday:
-(next_weekday (next_weekday saturday)) = tuesday.
-
-Proof. simpl. reflexivity. Qed.
-
-Inductive bool : Type :=
-	| true : bool
-	| false : bool.
-
-Definition negb (b:bool) : bool :=
-													 match b with
-																			 | true => false
-																			 | false => true
-													 end.
-
-Definition andb (b1:bool) (b2:bool) : bool :=
-		match b1 with
-		 | true => b2
-		 | false => false
-	  end.
-
-Definition orb (b1:bool) (b2:bool) : bool :=
-		match b1 with
-		  | true => true
-		  | false => b2
-		end.
-
-Example test_orb1: (orb true false) = true.
-Proof. simpl. reflexivity. Qed.
-
-Example test_orb2: (orb false false) = false.
-Proof. simpl. reflexivity. Qed.
-
-Example test_orb3: (orb false true) = true.
-Proof. simpl. reflexivity. Qed.
-
-Example test_orb4: (orb true true) = true.
-Proof. simpl. reflexivity. Qed.
-
-Definition nandb (b1: bool) (b2:bool) : bool :=
-	match b1 with
-		| true => match b2 with
-										| false => true
-										| true => false
-							end
-		| false => true
-	end.
-
-Example test_nandb1: (nandb true false) = true.
-Proof. simpl. reflexivity. Qed.
-Example test_nandb2: (nandb false false) = true.
-Proof. simpl. reflexivity. Qed.
-Example test_nandb3: (nandb false true) = true.
-Proof. simpl. reflexivity. Qed.
-Example test_nandb4: (nandb true true) = false.
-Proof. simpl. reflexivity. Qed.
-
-Definition andb3 (b1: bool) (b2:bool) (b3:bool) : bool :=
-	match b1 with
-    | false => false
-		| true => match b2 with
-								| false => false
-								| true => b3
-							end
-	end.
-
-Example test_andb31: (andb3 true true true) = true.
-Proof. simpl. reflexivity. Qed.
-Example test_andb32: (andb3 false true true) = false.
-Proof. simpl. reflexivity. Qed.
-Example test_andb33: (andb3 true false true) = false.
-Proof. simpl. reflexivity. Qed.
-Example test_andb34: (andb3 true true false) = false.
-Proof. simpl. reflexivity. Qed.
-
-Module Playground1.
-
-Inductive nat : Type :=
-	| O : nat
-	| S : nat -> nat.
-
-Definition pred (n : nat) : nat :=
-	match n with
-		| O => O
-		| S n' => n'
-	end.
-
-Definition minustwo (n : nat) : nat :=
-	match n with
-		| O => O
-		| S O => O
-		| S (S n') => n'
-	end.
-
-Fixpoint evenb (n : nat) : bool :=
-	match n with
-		| O => true
-		| S O => false
-		| S (S n') => evenb n'
-	end.
-
-Definition oddb (n : nat) : bool := negb (evenb n).
-
-Example test_oddb1: (oddb (S O)) = true.
-Proof. reflexivity. Qed.
-Example test_oddb2: (oddb (S (S (S (S O))))) = false.
-Proof. reflexivity. Qed.
-
-Fixpoint plus (n : nat) (m : nat) : nat :=
-	match n with
-		| O => m
-		| S n' => S (plus n' m)
-	end.
-
-Fixpoint mult (n m : nat) : nat :=
-	match n with
-		| O => O
-		| S n' => plus m (mult n' m)
-	end.
-
-Fixpoint minus (n m : nat) : nat :=
-	match n, m with
-		| O, _ => n
-		| S n', O => S n'
-		| S n', S m' => minus n' m'
-	end.
-
-Fixpoint exp (base power : nat) : nat :=
-	match power with
-		| O => S O
-		| S p => mult base (exp base p)
-	end.
-
-Fixpoint factorial (n : nat) : nat :=
-	match n with
-		| O => S O
-		| S n' => mult n (factorial n')
-	end.
-
-Example test_factorial1: (factorial (S (S (S O)))) = (S (S (S (S (S (S O)))))).
-Proof. simpl. reflexivity. Qed.
-
-Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope.
-Notation "x - y" := (minus x y) (at level 50, left associativity) : nat_scope.
-Notation "x * y" := (mult x y) (at level 40, left associativity) : nat_scope.
-
-Fixpoint beq_nat (n m : nat) : bool :=
-	match n with
-		| O => match m with
-						| O => true
-						| S m' => false
-					 end
-		| S n' => match m with
-							| O => false
-							| S m' => beq_nat n' m'
-							end
-	end.
-
-Fixpoint ble_nat (n m : nat) : bool :=
-	match n with
-		| O => true
-		| S n' => 
-				match m with
-					| O => false
-					| S m' => ble_nat n' m'
-				end
-	end.
-
-Example test_ble_nat1: (ble_nat (S (S O)) (S (S O))) = true.
-Proof. simpl. reflexivity. Qed.
-Example test_ble_nat2: (ble_nat (S (S O)) (S (S (S (S O))))) = true.
-Proof. simpl. reflexivity. Qed.
-Example test_ble_nat3: (ble_nat (S (S (S (S O)))) (S (S O))) = false.
-Proof. simpl. reflexivity. Qed.
-
-Definition blt_nat (n m : nat) : bool :=
-		(andb (negb (beq_nat n m)) (ble_nat n m)).
-
-Example test_blt_nat1: (blt_nat (S (S O)) (S (S O))) = false.
-Proof. simpl. reflexivity. Qed.
-Example test_blt_nat3: (blt_nat (S (S (S (S O)))) (S (S O))) = false.
-Proof. simpl. reflexivity. Qed.
-Example test_blt_nat2 : (blt_nat (S (S O)) (S (S (S (S O))))) = true.
-Proof. simpl. reflexivity. Qed.
-
-Theorem plus_O_n : forall n : nat, O + n = n.
-Proof.
-	simpl. reflexivity. Qed.
-
-Theorem plus_O_n' : forall n : nat, O + n = n.
-Proof.
-	reflexivity. Qed.
-
-Theorem plus_O_n'' : forall n : nat, O + n = n.
-Proof.
-	intros n. reflexivity. Qed.
-
-Theorem plus_1_1 : forall n : nat, (S O) + n = S n.
-Proof.
-	intros n. reflexivity. Qed.
-
-Theorem mult_0_1: forall n : nat, O * n = O.
-Proof.
-	intros n. reflexivity. Qed.
-
-Theorem plus_id_example : forall n m:nat,
-	n = m -> n + n = m + m.
-Proof.
-	intros n m.
-	intros H.
-	rewrite -> H.
-	reflexivity. Qed.
-
-Theorem plus_id_exercise : forall n m o: nat,
-	n = m -> m = o -> n + m = m + o.
-Proof.
-	intros n m o.
-	intros H.
-	intros H'.
-	rewrite -> H.
-	rewrite <- H'.
-	reflexivity.
-	Qed.
-
-Theorem mult_0_plus : forall n m : nat,
-				(O + n) * m = n * m.
-Proof.
-	intros n m.
-	rewrite -> plus_O_n.
-	reflexivity. Qed.
-
-Theorem mult_1_plus : forall n m: nat,
-	((S O) + n) * m = m + (n * m).
-Proof.
-	intros n m.
-	rewrite -> plus_1_1.
-	reflexivity.
-	Qed.
-
-Theorem mult_1 : forall n : nat,
-				n * (S O) = n.
-Proof.
-	intros n.
-	induction n as [| n'].
-	reflexivity.
-	simpl.
-	rewrite -> IHn'.
-	reflexivity.
-	Qed.
-
-Theorem plus_1_neq_0 : forall n : nat,
-				beq_nat (n + (S O)) O = false.
-Proof.
-	intros n.
-	destruct n as [| n'].
-	reflexivity.
-	reflexivity.
-	Qed.
-
-Theorem zero_nbeq_plus_1 : forall n : nat,
-				beq_nat O (n + (S O)) = false.
-Proof.
-	intros n.
-	destruct n.
-	reflexivity.
-	reflexivity.
-Qed.
-
-Require String. Open Scope string_scope.
-
-Ltac move_to_top x :=
-match reverse goal with
-| H : _ |- _ => try move x after H
-end.
-
-Tactic Notation "assert_eq" ident(x) constr(v) :=
-	let H := fresh in
-	assert (x = v) as H by reflexivity;
-	clear H.
-
-	Tactic Notation "Case_aux" ident(x) constr(name) :=
-		first [
-		set (x := name); move_to_top x
-		| assert_eq x name; move_to_top x
-		| fail 1 "because we are working on a different case" ].
-
-		Ltac Case name := Case_aux Case name.
-		Ltac SCase name := Case_aux SCase name.
-		Ltac SSCase name := Case_aux SSCase name.
-		Ltac SSSCase name := Case_aux SSSCase name.
-		Ltac SSSSCase name := Case_aux SSSSCase name.
-		Ltac SSSSSCase name := Case_aux SSSSSCase name.
-		Ltac SSSSSSCase name := Case_aux SSSSSSCase name.
-		Ltac SSSSSSSCase name := Case_aux SSSSSSSCase name.
-
-Theorem andb_true_elim1 : forall b c : bool,
-				andb b c = true -> b = true.
-Proof.
-	intros b c H.
-	destruct b.
-	Case "b = true".
-		reflexivity.
-	Case "b = false".
-		rewrite <- H. reflexivity. Qed.
-
-Theorem plus_0_r : forall n : nat, n + O = n.
-Proof.
-	intros n. induction n as [| n'].
-	Case "n = 0". reflexivity.
-	Case "n = S n'". simpl. rewrite -> IHn'. reflexivity. Qed.
-
-Theorem minus_diag : forall n,
-				minus n n = O.
-Proof.
-	intros n. induction n as [| n'].
-	Case "n = 0".
-		simpl. reflexivity.
-	Case "n = S n'".
-		simpl. rewrite -> IHn'. reflexivity. Qed.
-
-
-Theorem mult_0_r : forall n:nat,
-				n * O = O.
-Proof.
-	intros n. induction n as [| n'].
-	Case "n = 0".
-		reflexivity.
-	Case "n = S n'".
-		simpl. rewrite -> IHn'. reflexivity. Qed.
-
-Theorem plus_n_Sm : forall n m : nat,
-				S (n + m) = n + (S m).
-Proof.
-	intros n m. induction n as [| n'].
-	Case "n = 0".
-		reflexivity.
-	Case "n = S n'".
-		simpl. rewrite -> IHn'. reflexivity. Qed.
-
-Theorem plus_assoc : forall n m p : nat,
-					n + (m + p) = (n + m) + p.
-Proof.
-	intros n m p.
-	induction n as [| n'].
-	reflexivity.
-	simpl.
-	rewrite -> IHn'.
-	reflexivity. Qed.
-
-Theorem plus_distr : forall n m: nat, S (n + m) = n + (S m).
-Proof.
-	intros n m.  induction n as [| n'].
-	Case "n = 0".
-		reflexivity.
-	Case "n = S n'".
-		simpl. rewrite -> IHn'. reflexivity. Qed.
-
-Theorem mult_distr : forall n m: nat, n * ((S O) + m) = n * (S m).
-Proof.
-	intros n m.
-	induction n as [| n'].
-	reflexivity.
-	reflexivity.
-	Qed.
-
-Theorem plus_comm : forall n m : nat,
-	n + m = m + n.
-Proof.
-	intros n m.
-	induction n as [| n'].
-	Case "n = 0".
-		simpl.
-		rewrite -> plus_0_r.
-		reflexivity.
-	Case "n = S n'".
-		simpl.
-		rewrite -> IHn'.
-		rewrite -> plus_distr.
-		reflexivity. Qed.
-
-Fixpoint double (n:nat) :=
-	match n with
-		| O => O
-		| S n' => S (S (double n'))
-	end.
-
-Lemma double_plus : forall n, double n = n + n.
-Proof.
-	intros n. induction n as [| n'].
-	Case "n = 0".
-		reflexivity.
-	Case "n = S n'".
-		simpl. rewrite -> IHn'.
-		rewrite -> plus_distr. reflexivity.
-		Qed.
-
-Theorem beq_nat_refl : forall n : nat,
-	true = beq_nat n n.
-Proof.
-	intros n. induction n as [| n'].
-	Case "n = 0".
-		reflexivity.
-	Case "n = S n".
-		simpl. rewrite <- IHn'.
-		reflexivity. Qed.
-
-Theorem plus_rearrange: forall n m p q : nat,
-				(n + m) + (p + q) = (m + n) + (p + q).
-Proof.
-	intros n m p q.
-	assert(H: n + m = m + n).
-		Case "Proof by assertion".
-		rewrite -> plus_comm. reflexivity.
-	rewrite -> H. reflexivity. Qed.
-
-Theorem plus_swap : forall n m p: nat,
-				n + (m + p) = m + (n + p).
-Proof.
-	intros n m p.
-	rewrite -> plus_assoc.
-	assert(H: m + (n + p) = (m + n) + p).
-	rewrite -> plus_assoc.
-	reflexivity.
-	rewrite -> H.
-	assert(H2: m + n = n + m).
-	rewrite -> plus_comm.
-	reflexivity.
-	rewrite -> H2.
-	reflexivity.
-	Qed.
-
-Theorem plus_swap' : forall n m p: nat,
-				n + (m + p) = m + (n + p).
-Proof.
-	intros n m p.
-	rewrite -> plus_assoc.
-	assert(H: m + (n + p) = (m + n) + p).
-	rewrite -> plus_assoc.
-	reflexivity.
-	rewrite -> H.
-	replace (m + n) with (n + m).
-	rewrite -> plus_comm.
-	reflexivity.
-	rewrite -> plus_comm.
-	reflexivity.
-	Qed.
-
-Theorem mult_1_distr: forall m n: nat,
-				n * ((S O) + m) = n * (S O) + n * m.
-Proof.
-	intros n m.
-	rewrite -> mult_1.
-	rewrite -> plus_1_1.
-	simpl.
-	induction m as [|m'].
-	simpl.
-	reflexivity.
-	simpl.
-	rewrite -> plus_swap.
-	rewrite <- IHm'.
-	reflexivity.
-	Qed.
-
-Theorem mult_comm: forall m n : nat,
-				m * n = n * m.
-Proof.
-	intros m n.
-	induction n as [| n'].
-	Case "n = 0".
-		simpl.
-		rewrite -> mult_0_r.
-		reflexivity.
-	Case "n = S n'".
-		simpl.
-		rewrite <- mult_distr.
-		rewrite -> mult_1_distr.
-		rewrite -> mult_1.
-		rewrite -> IHn'.
-		reflexivity.
-		Qed.
-
-Theorem evenb_next : forall n : nat,
-				evenb n = evenb (S (S n)).
-Proof.
-	intros n.
-Admitted.
-
-Theorem negb_negb : forall n : bool,
-				n = negb (negb n).
-Proof.
-	intros n.
-	destruct n.
-	reflexivity.
-	reflexivity.
-	Qed.
-
-Theorem evenb_n_oddb_Sn : forall n : nat,
-				evenb n = negb (evenb (S n)).
-Proof.
-	intros n.
-	induction n as [|n'].
-	reflexivity.
-	assert(H: evenb n' = evenb (S (S n'))).
-	reflexivity.
-	rewrite <- H.
-	rewrite -> IHn'.
-	rewrite <- negb_negb.
-	reflexivity.
-	Qed.
-
-(*Fixpoint bad (n : nat) : bool :=
-	match n with
-		| O => true
-		| S O => bad (S n)
-		| S (S n') => bad n'
-	end.*)
-
-Theorem ble_nat_refl : forall n:nat,
-				true = ble_nat n n.
-Proof.
-	intros n.
-	induction n as [|n'].
-	Case "n = 0".
-		reflexivity.
-	Case "n = S n".
-		simpl.
-		rewrite <- IHn'.
-		reflexivity.
-	Qed.
-
-Theorem zero_nbeq_S : forall n: nat,
-				beq_nat O (S n) = false.
-Proof.
-	intros n.
-	reflexivity.
-	Qed.
-
-Theorem andb_false_r : forall b : bool,
-				andb b false = false.
-Proof.
-	intros b.
-	destruct b.
-	reflexivity.
-	reflexivity.
-	Qed.
-
-Theorem plus_ble_compat_1 : forall n m p : nat,
-				ble_nat n m = true -> ble_nat (p + n) (p + m) = true.
-Proof.
-	intros n m p.
-	intros H.
-	induction p.
-	Case "p = 0".
-		simpl.
-		rewrite -> H.
-		reflexivity.
-	Case "p = S p'".
-		simpl.
-		rewrite -> IHp.
-		reflexivity.
-		Qed.
-
-Theorem S_nbeq_0 : forall n:nat,
-				beq_nat (S n) O = false.
-Proof.
-	intros n.
-	reflexivity.
-	Qed.
-
-Theorem mult_1_1 : forall n:nat, (S O) * n = n.
-Proof.
-	intros n.
-	simpl.
-	rewrite -> plus_0_r.
-	reflexivity. Qed.
-
-Theorem all3_spec : forall b c : bool,
-	orb (andb b c)
-			(orb (negb b)
-			 		 (negb c))
-	= true.
-Proof.
-	intros b c.
-	destruct b.
-	destruct c.
-	reflexivity.
-	reflexivity.
-	reflexivity.
-	Qed.
-
-Lemma mult_plus_1 : forall n m : nat,
-			S(m + n) = m + (S n).
-Proof.
-	intros n m.
-	induction m.
-	reflexivity.
-	simpl.
-	rewrite -> IHm.
-	reflexivity.
-	Qed.
-
-Theorem mult_mult : forall n m : nat,
-	n * (S m) = n * m + n.
-Proof.
-	intros n m.
-	induction n.
-	reflexivity.
-	simpl.
-	rewrite -> IHn.
-	rewrite -> plus_assoc.
-	rewrite -> mult_plus_1.
-	reflexivity.
-	Qed.
-
-Theorem mult_plus_distr_r : forall n m p:nat,
-				(n + m) * p = (n * p) + (m * p).
-Proof.
-	intros n m p.
-	induction p.
-	rewrite -> mult_0_r.
-	rewrite -> mult_0_r.
-	rewrite -> mult_0_r.
-	reflexivity.
-	rewrite -> mult_mult.
-	rewrite -> mult_mult.
-	rewrite -> mult_mult.
-	rewrite -> IHp.
-	assert(H1: ((n * p) + n) + (m * p + m) = (n * p) + (n + (m * p + m))).
-	rewrite <- plus_assoc.
-	reflexivity.
-	rewrite -> H1.
-	assert(H2: (n + (m * p + m)) = (m * p + (n + m))).
-	rewrite -> plus_swap.
-	reflexivity.
-	rewrite -> H2.
-	assert(H3: (n * p) + (m * p + (n + m)) = ((n * p ) + (m * p)) + (n + m)).
-	rewrite -> plus_assoc.
-	reflexivity.
-	rewrite -> H3.
-	reflexivity.
-	Qed.
-
-Theorem mult_assoc : forall n m p : nat,
-				n * (m * p) = (n * m) * p.
-Proof.
-	intros n m p.
-	induction n.
-	simpl.
-	reflexivity.
-	simpl.
-	rewrite -> mult_plus_distr_r.
-	rewrite -> IHn.
-	reflexivity.
-	Qed.
-
-Inductive bin : Type :=
-	| BO : bin
-	| D : bin -> bin
-	| M : bin -> bin.
-
-Fixpoint incbin (n : bin) : bin :=
-	match n with
-		| BO => M (BO)
-		| D n' => M n'
-		| M n' => D (incbin n')
-	end.
-
-Fixpoint bin2un (n : bin) : nat :=
-	match n with
-		| BO => O
-		| D n' => double (bin2un n')
-		| M n' => S (double (bin2un n'))
-	end.
-
-Theorem bin_comm : forall n : bin,
-				bin2un(incbin n) = S (bin2un n).
-Proof.
-	intros n.
-	induction n.
-		reflexivity.
-		reflexivity.
-		simpl.
-		rewrite -> IHn.
-		reflexivity.
-	Qed.
-
-End Playground1.
diff --git a/samples/Coq/Heap.v b/samples/Coq/Heap.v
deleted file mode 100755
index 4881c99e..00000000
--- a/samples/Coq/Heap.v
+++ /dev/null
@@ -1,290 +0,0 @@
-(** 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.
-  Hint Immediate eqA_dec leA_dec leA_antisym.
-
-  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.
-  Proof.
-    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).
-  Proof.
-    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.
-  Proof.
-    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.
-  Proof.
-    simple induction T; auto with datatypes.
-    intros a G PG D PD PN.
-    elim (invert_heap a G D); auto with datatypes.
-    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
-    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.
-  Proof.
-    simple induction T; auto with datatypes.
-    intros a G PG D PD PN.
-    elim (invert_heap a G D); auto with datatypes.
-    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
-    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.
-  Proof.
-    simple induction T; auto with datatypes.
-    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.
-  Require Import Morphisms.
-
-  Instance: Equivalence (@meq A).
-  Proof. constructor; auto with datatypes. red. apply meq_trans. Defined.
-
-  Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A).
-  Proof. intros x y H x' y' H'. 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.
-  Proof.
-    fix 1; intros; destruct l1.
-    apply merge_exist with l2; auto with datatypes.
-    rename l1 into l.
-    revert l2 H0. fix 1. intros.
-    destruct l2 as [|a0 l0].
-    apply merge_exist with (a :: l); simpl; auto with datatypes.
-    elim (leA_dec a a0); intros.
-
-    (* 1 (leA a a0) *)
-    apply Sorted_inv in H. destruct H.
-    destruct (merge l H (a0 :: l0) H0).
-    apply merge_exist with (a :: l1). clear merge merge0.
-      auto using cons_sort, cons_leA with datatypes.
-    simpl. rewrite m. now rewrite munion_ass.
-    intros. apply cons_leA.
-    apply (@HdRel_inv _ leA) with l; trivial with datatypes.
-
-    (* 2 (leA a0 a) *)
-    apply Sorted_inv in H0. destruct H0.
-    destruct (merge0 l0 H0). clear merge merge0.
-    apply merge_exist with (a0 :: l1);
-      auto using cons_sort, cons_leA with datatypes.
-    simpl; rewrite m. simpl. setoid_rewrite munion_ass at 1. rewrite munion_comm.
-    repeat rewrite munion_ass. setoid_rewrite munion_comm at 3. reflexivity.
-    intros. apply cons_leA.
-    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.
-  Proof.
-    simple induction 1; intros.
-    apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
-      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
-    simpl; unfold meq, munion; auto using node_is_heap with datatypes.
-    elim (leA_dec a a0); intros.
-    elim (X a0); intros.
-    apply insert_exist with (Tree_Node a T2 T0);
-      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
-    simpl; apply treesort_twist1; trivial with datatypes.
-    elim (X a); intros T3 HeapT3 ConT3 LeA.
-    apply insert_exist with (Tree_Node a0 T2 T3);
-      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
-    apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
-    apply low_trans with a; auto with datatypes.
-    apply LeA; auto with datatypes.
-    apply low_trans with a; auto with datatypes.
-    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.
-  Proof.
-    simple induction l.
-    apply (heap_exist nil Tree_Leaf); auto with datatypes.
-    simpl; unfold meq; exact nil_is_heap.
-    simple induction 1.
-    intros T i m; elim (insert T i a).
-    intros; apply heap_exist with T1; simpl; auto with datatypes.
-    apply meq_trans with (munion (contents T) (singletonBag a)).
-    apply meq_trans with (munion (singletonBag a) (contents T)).
-    apply meq_right; trivial with datatypes.
-    apply munion_comm.
-    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.
-  Proof.
-    intros T h; elim h; intros.
-    apply flat_exist with (nil (A:=A)); auto with datatypes.
-    elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2.
-    elim (merge _ s1 _ s2); intros.
-    apply flat_exist with (a :: l); simpl; auto with datatypes.
-    apply meq_trans with
-      (munion (list_contents _ eqA_dec l1)
-        (munion (list_contents _ eqA_dec l2) (singletonBag a))).
-    apply meq_congr; auto with datatypes.
-    apply meq_trans with
-      (munion (singletonBag a)
-        (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
-    apply munion_rotate.
-    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}.
-  Proof.
-    intro l; unfold permutation.
-    elim (list_to_heap l).
-    intros.
-    elim (heap_to_list T); auto with datatypes.
-    intros.
-    exists l0; auto with datatypes.
-    apply meq_trans with (contents T); trivial with datatypes.
-  Qed.
-
-End defs.
diff --git a/samples/Coq/PermutSetoid.v b/samples/Coq/PermutSetoid.v
deleted file mode 100755
index 2e0dd17f..00000000
--- a/samples/Coq/PermutSetoid.v
+++ /dev/null
@@ -1,539 +0,0 @@
-Require Import Omega Relations Multiset SetoidList.
-
-(** This file is deprecated, use [Permutation.v] instead.
-
-    Indeed, this file defines a notion of permutation based on
-    multisets (there exists a permutation between two lists iff every
-    elements have the same multiplicity in the two lists) which
-    requires a more complex apparatus (the equipment of the domain
-    with a decidable equality) than [Permutation] in [Permutation.v].
-
-    The relation between the two relations are in lemma
-    [permutation_Permutation].
-
-    File [Permutation] concerns Leibniz equality : it shows in particular
-    that [List.Permutation] and [permutation] are equivalent in this context.
-*)
-
-Set Implicit Arguments.
-
-Local Notation "[ ]" := nil.
-Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..).
-
-Section Permut.
-
-(** * From lists to multisets *)
-
-Variable A : Type.
-Variable eqA : relation A.
-Hypothesis eqA_equiv : Equivalence eqA.
-Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
-
-Let emptyBag := EmptyBag A.
-Let singletonBag := SingletonBag _ eqA_dec.
-
-(** contents of a list *)
-
-Fixpoint list_contents (l:list A) : multiset A :=
-  match l with
-  | [] => emptyBag
-  | a :: l => munion (singletonBag a) (list_contents l)
-  end.
-
-Lemma list_contents_app :
-  forall l m:list A,
-    meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
-Proof.
-  simple induction l; simpl; auto with datatypes.
-  intros.
-  apply meq_trans with
-    (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
-    auto with datatypes.
-Qed.
-
-(** * [permutation]: definition and basic properties *)
-
-Definition permutation (l m:list A) := meq (list_contents l) (list_contents m).
-
-Lemma permut_refl : forall l:list A, permutation l l.
-Proof.
-  unfold permutation; auto with datatypes.
-Qed.
-
-Lemma permut_sym :
-  forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
-Proof.
-  unfold permutation, meq; intros; symmetry; trivial.
-Qed.
-
-Lemma permut_trans :
-  forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
-Proof.
-  unfold permutation; intros.
-  apply meq_trans with (list_contents m); auto with datatypes.
-Qed.
-
-Lemma permut_cons_eq :
-  forall l m:list A,
-    permutation l m -> forall a a', eqA a a' -> permutation (a :: l) (a' :: m).
-Proof.
-  unfold permutation; simpl; intros.
-  apply meq_trans with (munion (singletonBag a') (list_contents l)).
-  apply meq_left, meq_singleton; auto.
-  auto with datatypes.
-Qed.
-
-Lemma permut_cons :
-  forall l m:list A,
-    permutation l m -> forall a:A, permutation (a :: l) (a :: m).
-Proof.
-  unfold permutation; simpl; auto with datatypes.
-Qed.
-
-Lemma permut_app :
-  forall l l' m m':list A,
-    permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
-Proof.
-  unfold permutation; intros.
-  apply meq_trans with (munion (list_contents l) (list_contents m));
-    auto using permut_cons, list_contents_app with datatypes.
-  apply meq_trans with (munion (list_contents l') (list_contents m'));
-    auto using permut_cons, list_contents_app with datatypes.
-  apply meq_trans with (munion (list_contents l') (list_contents m));
-    auto using permut_cons, list_contents_app with datatypes.
-Qed.
-
-Lemma permut_add_inside_eq :
-  forall a a' l1 l2 l3 l4, eqA a a' ->
-    permutation (l1 ++ l2) (l3 ++ l4) ->
-    permutation (l1 ++ a :: l2) (l3 ++ a' :: l4).
-Proof.
-  unfold permutation, meq in *; intros.
-  specialize H0 with a0.
-  repeat rewrite list_contents_app in *; simpl in *.
-  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite H in Ha;
-    decide (eqA_dec a' a0) with Ha; simpl; auto with arith.
-  do 2 rewrite <- plus_n_Sm; f_equal; auto.
-Qed.
-
-Lemma permut_add_inside :
-  forall a l1 l2 l3 l4,
-    permutation (l1 ++ l2) (l3 ++ l4) ->
-    permutation (l1 ++ a :: l2) (l3 ++ a :: l4).
-Proof.
-  unfold permutation, meq in *; intros.
-  generalize (H a0); clear H.
-  do 4 rewrite list_contents_app.
-  simpl.
-  destruct (eqA_dec a a0); simpl; auto with arith.
-  do 2 rewrite <- plus_n_Sm; f_equal; auto.
-Qed.
-
-Lemma permut_add_cons_inside_eq :
-  forall a a' l l1 l2, eqA a a' ->
-    permutation l (l1 ++ l2) ->
-    permutation (a :: l) (l1 ++ a' :: l2).
-Proof.
-  intros;
-  replace (a :: l) with ([] ++ a :: l); trivial;
-    apply permut_add_inside_eq; trivial.
-Qed.
-
-Lemma permut_add_cons_inside :
-  forall a l l1 l2,
-    permutation l (l1 ++ l2) ->
-    permutation (a :: l) (l1 ++ a :: l2).
-Proof.
-  intros;
-    replace (a :: l) with ([] ++ a :: l); trivial;
-        apply permut_add_inside; trivial.
-Qed.
-
-Lemma permut_middle :
-  forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
-Proof.
-  intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl.
-Qed.
-
-Lemma permut_sym_app :
-  forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
-Proof.
-  intros l1 l2;
-    unfold permutation, meq;
-        intro a; do 2 rewrite list_contents_app; simpl;
-          auto with arith.
-Qed.
-
-Lemma permut_rev :
-  forall l, permutation l (rev l).
-Proof.
-  induction l.
-  simpl; trivial using permut_refl.
-  simpl.
-  apply permut_add_cons_inside.
-  rewrite <- app_nil_end. trivial.
-Qed.
-
-(** * Some inversion results. *)
-Lemma permut_conv_inv :
-  forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.
-Proof.
-  intros e l1 l2; unfold permutation, meq; simpl; intros H a;
-    generalize (H a); apply plus_reg_l.
-Qed.
-
-Lemma permut_app_inv1 :
-  forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.
-Proof.
-  intros l l1 l2; unfold permutation, meq; simpl;
-    intros H a; generalize (H a); clear H.
-  do 2 rewrite list_contents_app.
-  simpl.
-  intros; apply plus_reg_l with (multiplicity (list_contents l) a).
-  rewrite plus_comm; rewrite H; rewrite plus_comm.
-  trivial.
-Qed.
-
-(** we can use [multiplicity] to define [InA] and [NoDupA]. *)
-
-Fact if_eqA_then : forall a a' (B:Type)(b b':B),
- eqA a a' -> (if eqA_dec a a' then b else b') = b.
-Proof.
-  intros. destruct eqA_dec as [_|NEQ]; auto.
-  contradict NEQ; auto.
-Qed.
-
-Lemma permut_app_inv2 :
-  forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.
-Proof.
-  intros l l1 l2; unfold permutation, meq; simpl;
-    intros H a; generalize (H a); clear H.
-  do 2 rewrite list_contents_app.
-  simpl.
-  intros; apply plus_reg_l with (multiplicity (list_contents l) a).
-  trivial.
-Qed.
-
-Lemma permut_remove_hd_eq :
-  forall l l1 l2 a b, eqA a b ->
-    permutation (a :: l) (l1 ++ b :: l2) -> permutation l (l1 ++ l2).
-Proof.
-  unfold permutation, meq; simpl; intros l l1 l2 a b Heq H a0.
-  specialize H with a0.
-  rewrite list_contents_app in *; simpl in *.
-  apply plus_reg_l with (if eqA_dec a a0 then 1 else 0).
-  rewrite H; clear H.
-  symmetry; rewrite plus_comm, <- ! plus_assoc; f_equal.
-  rewrite plus_comm.
-  destruct (eqA_dec a a0) as [Ha|Ha]; rewrite Heq in Ha;
-    decide (eqA_dec b a0) with Ha; reflexivity.
-Qed.
-
-Lemma permut_remove_hd :
-  forall l l1 l2 a,
-    permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
-Proof.
-  eauto using permut_remove_hd_eq, Equivalence_Reflexive.
-Qed.
-
-Fact if_eqA_else : forall a a' (B:Type)(b b':B),
- ~eqA a a' -> (if eqA_dec a a' then b else b') = b'.
-Proof.
-  intros. decide (eqA_dec a a') with H; auto.
-Qed.
-
-Fact if_eqA_refl : forall a (B:Type)(b b':B),
- (if eqA_dec a a then b else b') = b.
-Proof.
-  intros; apply (decide_left (eqA_dec a a)); auto with *.
-Qed.
-
-(** PL: Inutilisable dans un rewrite sans un change prealable. *)
-
-Global Instance if_eqA (B:Type)(b b':B) :
- Proper (eqA==>eqA==>@eq _) (fun x y => if eqA_dec x y then b else b').
-Proof.
- intros x x' Hxx' y y' Hyy'.
- intros; destruct (eqA_dec x y) as [H|H];
-  destruct (eqA_dec x' y') as [H'|H']; auto.
- contradict H'; transitivity x; auto with *; transitivity y; auto with *.
- contradict H; transitivity x'; auto with *; transitivity y'; auto with *.
-Qed.
-
-Fact if_eqA_rewrite_l : forall a1 a1' a2 (B:Type)(b b':B),
- eqA a1 a1' -> (if eqA_dec a1 a2 then b else b') =
-               (if eqA_dec a1' a2 then b else b').
-Proof.
- intros; destruct (eqA_dec a1 a2) as [A1|A1];
-  destruct (eqA_dec a1' a2) as [A1'|A1']; auto.
- contradict A1'; transitivity a1; eauto with *.
- contradict A1; transitivity a1'; eauto with *.
-Qed.
-
-Fact if_eqA_rewrite_r : forall a1 a2 a2' (B:Type)(b b':B),
- eqA a2 a2' -> (if eqA_dec a1 a2 then b else b') =
-               (if eqA_dec a1 a2' then b else b').
-Proof.
- intros; destruct (eqA_dec a1 a2) as [A2|A2];
-  destruct (eqA_dec a1 a2') as [A2'|A2']; auto.
- contradict A2'; transitivity a2; eauto with *.
- contradict A2; transitivity a2'; eauto with *.
-Qed.
-
-
-Global Instance multiplicity_eqA (l:list A) :
- Proper (eqA==>@eq _) (multiplicity (list_contents l)).
-Proof.
-  intros x x' Hxx'.
-  induction l as [|y l Hl]; simpl; auto.
-  rewrite (@if_eqA_rewrite_r y x x'); auto.
-Qed.
-
-Lemma multiplicity_InA :
-  forall l a, InA eqA a l <-> 0 < multiplicity (list_contents l) a.
-Proof.
-  induction l.
-  simpl.
-  split; inversion 1.
-  simpl.
-  intros a'; split; intros H. inversion_clear H.
-  apply (decide_left (eqA_dec a a')); auto with *.
-  destruct (eqA_dec a a'); auto with *. simpl; rewrite <- IHl; auto.
-  destruct (eqA_dec a a'); auto with *. right. rewrite IHl; auto.
-Qed.
-
-Lemma multiplicity_InA_O :
-  forall l a, ~ InA eqA a l -> multiplicity (list_contents l) a = 0.
-Proof.
-  intros l a; rewrite multiplicity_InA;
-    destruct (multiplicity (list_contents l) a); auto with arith.
-  destruct 1; auto with arith.
-Qed.
-
-Lemma multiplicity_InA_S :
-  forall l a, InA eqA a l -> multiplicity (list_contents l) a >= 1.
-Proof.
-  intros l a; rewrite multiplicity_InA; auto with arith.
-Qed.
-
-Lemma multiplicity_NoDupA : forall l,
-  NoDupA eqA l <-> (forall a, multiplicity (list_contents l) a <= 1).
-Proof.
-  induction l.
-  simpl.
-  split; auto with arith.
-  split; simpl.
-  inversion_clear 1.
-  rewrite IHl in H1.
-  intros; destruct (eqA_dec a a0) as [EQ|NEQ]; simpl; auto with *.
-  rewrite <- EQ.
-  rewrite multiplicity_InA_O; auto.
-  intros; constructor.
-  rewrite multiplicity_InA.
-  specialize (H a).
-  rewrite if_eqA_refl in H.
-  clear IHl; omega.
-  rewrite IHl; intros.
-  specialize (H a0). omega.
-Qed.
-
-(** Permutation is compatible with InA. *)
-Lemma permut_InA_InA :
-  forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.
-Proof.
-  intros l1 l2 e.
-  do 2 rewrite multiplicity_InA.
-  unfold permutation, meq.
-  intros H;rewrite H; auto.
-Qed.
-
-Lemma permut_cons_InA :
-  forall l1 l2 e, permutation (e :: l1) l2 -> InA eqA e l2.
-Proof.
-  intros; apply (permut_InA_InA (e:=e) H); auto with *.
-Qed.
-
-(** Permutation of an empty list. *)
-Lemma permut_nil :
-  forall l, permutation l [] -> l = [].
-Proof.
-  intro l; destruct l as [ | e l ]; trivial.
-  assert (InA eqA e (e::l)) by (auto with *).
-  intro Abs; generalize (permut_InA_InA Abs H).
-  inversion 1.
-Qed.
-
-(** Permutation for short lists. *)
-
-Lemma permut_length_1:
-  forall a b, permutation [a] [b] -> eqA a b.
-Proof.
-  intros a b; unfold permutation, meq.
-  intro P; specialize (P b); simpl in *.
-  rewrite if_eqA_refl in *.
-  destruct (eqA_dec a b); simpl; auto; discriminate.
-Qed.
-
-Lemma permut_length_2 :
-  forall a1 b1 a2 b2, permutation [a1; b1] [a2; b2] ->
-    (eqA a1 a2) /\ (eqA b1 b2) \/ (eqA a1 b2) /\ (eqA a2 b1).
-Proof.
-  intros a1 b1 a2 b2 P.
-  assert (H:=permut_cons_InA P).
-  inversion_clear H.
-  left; split; auto.
-  apply permut_length_1.
-  red; red; intros.
-  specialize (P a). simpl in *.
-  rewrite (@if_eqA_rewrite_l a1 a2 a) in P by auto. omega.
-  right.
-  inversion_clear H0; [|inversion H].
-  split; auto.
-  apply permut_length_1.
-  red; red; intros.
-  specialize (P a); simpl in *.
-  rewrite (@if_eqA_rewrite_l a1 b2 a) in P by auto. omega.
-Qed.
-
-(** Permutation is compatible with length. *)
-Lemma permut_length :
-  forall l1 l2, permutation l1 l2 -> length l1 = length l2.
-Proof.
-  induction l1; intros l2 H.
-  rewrite (permut_nil (permut_sym H)); auto.
-  assert (H0:=permut_cons_InA H).
-  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
-  subst l2.
-  rewrite app_length.
-  simpl; rewrite <- plus_n_Sm; f_equal.
-  rewrite <- app_length.
-  apply IHl1.
-  apply permut_remove_hd with b.
-  apply permut_trans with (a::l1); auto.
-  revert H1; unfold permutation, meq; simpl.
-  intros; f_equal; auto.
-  rewrite (@if_eqA_rewrite_l a b a0); auto.
-Qed.
-
-Lemma NoDupA_equivlistA_permut :
-  forall l l', NoDupA eqA l -> NoDupA eqA l' ->
-    equivlistA eqA l l' -> permutation l l'.
-Proof.
-  intros.
-  red; unfold meq; intros.
-  rewrite multiplicity_NoDupA in H, H0.
-  generalize (H a) (H0 a) (H1 a); clear H H0 H1.
-  do 2 rewrite multiplicity_InA.
-  destruct 3; omega.
-Qed.
-
-End Permut.
-
-Section Permut_map.
-
-Variables A B : Type.
-
-Variable eqA : relation A.
-Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
-Hypothesis eqA_equiv : Equivalence eqA.
-
-Variable eqB : B->B->Prop.
-Hypothesis eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
-Hypothesis eqB_trans : Transitive eqB.
-
-(** Permutation is compatible with map. *)
-
-Lemma permut_map :
-  forall f,
-    (Proper (eqA==>eqB) f) ->
-    forall l1 l2, permutation _ eqA_dec l1 l2 ->
-      permutation _ eqB_dec (map f l1) (map f l2).
-Proof.
-  intros f; induction l1.
-  intros l2 P; rewrite (permut_nil eqA_equiv (permut_sym P)); apply permut_refl.
-  intros l2 P.
-  simpl.
-  assert (H0:=permut_cons_InA eqA_equiv P).
-  destruct (InA_split H0) as (h2,(b,(t2,(H1,H2)))).
-  subst l2.
-  rewrite map_app.
-  simpl.
-  apply permut_trans with (f b :: map f l1).
-  revert H1; unfold permutation, meq; simpl.
-  intros; f_equal; auto.
-  destruct (eqB_dec (f b) a0) as [H2|H2];
-    destruct (eqB_dec (f a) a0) as [H3|H3]; auto.
-  destruct H3; transitivity (f b); auto with *.
-  destruct H2; transitivity (f a); auto with *.
-  apply permut_add_cons_inside.
-  rewrite <- map_app.
-  apply IHl1; auto.
-  apply permut_remove_hd with b; trivial.
-  apply permut_trans with (a::l1); auto.
-  revert H1; unfold permutation, meq; simpl.
-  intros; f_equal; auto.
-  rewrite (@if_eqA_rewrite_l _ _ eqA_equiv eqA_dec a b a0); auto.
-Qed.
-
-End Permut_map.
-
-Require Import Permutation.
-
-Section Permut_permut.
-
-Variable A : Type.
-
-Variable eqA : relation A.
-Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
-Hypothesis eqA_equiv : Equivalence eqA.
-
-Lemma Permutation_impl_permutation : forall l l',
-  Permutation l l' -> permutation _ eqA_dec l l'.
-Proof.
-  induction 1.
-    apply permut_refl.
-    apply permut_cons; auto using Equivalence_Reflexive.
-    change (x :: y :: l) with ([x] ++ y :: l);
-      apply permut_add_cons_inside; simpl;
-      apply permut_cons_eq; auto using Equivalence_Reflexive, permut_refl.
-    apply permut_trans with l'; trivial.
-Qed.
-
-Lemma permut_eqA : forall l l', Forall2 eqA l l' -> permutation _ eqA_dec l l'.
-Proof.
-  induction 1.
-    apply permut_refl.
-    apply permut_cons_eq; trivial.
-Qed.
-
-Lemma permutation_Permutation : forall l l',
-  permutation _ eqA_dec l l' <->
-  exists l'', Permutation l l'' /\ Forall2 eqA l'' l'.
-Proof.
-  split; intro H.
-  (* -> *)
-  induction l in l', H |- *.
-    exists []; apply permut_sym, permut_nil in H as ->; auto using Forall2.
-    pose proof H as H'.
-    apply permut_cons_InA, InA_split in H
-      as (l1 & y & l2 & Heq & ->); trivial.
-    apply permut_remove_hd_eq, IHl in H'
-      as (l'' & IHP & IHA); clear IHl; trivial.
-    apply Forall2_app_inv_r in IHA as (l1'' & l2'' & Hl1 & Hl2 & ->).
-    exists (l1'' ++ a :: l2''); split.
-      apply Permutation_cons_app; trivial.
-      apply Forall2_app, Forall2_cons; trivial.
-  (* <- *)
-  destruct H as (l'' & H & Heq).
-  apply permut_trans with l''.
-    apply Permutation_impl_permutation; trivial.
-    apply permut_eqA; trivial.
-Qed.
-
-End Permut_permut.
-
-(* begin hide *)
-(** For compatibilty *)
-Notation permut_right := permut_cons (only parsing).
-Notation permut_tran := permut_trans (only parsing).
-(* end hide *)
diff --git a/samples/Coq/Permutation.v b/samples/Coq/Permutation.v
deleted file mode 100755
index 4761fb6d..00000000
--- a/samples/Coq/Permutation.v
+++ /dev/null
@@ -1,632 +0,0 @@
-(* Adapted in May 2006 by Jean-Marc Notin from initial contents by
-   Laurent Thery (Huffmann contribution, October 2003) *)
-
-Require Import List Setoid Compare_dec Morphisms.
-Import ListNotations. (* For notations [] and [a;b;c] *)
-Set Implicit Arguments.
-
-Section Permutation.
-
-Variable A:Type.
-
-Inductive Permutation : list A -> list A -> Prop :=
-| perm_nil: Permutation [] []
-| perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
-| perm_swap x y l : Permutation (y::x::l) (x::y::l)
-| perm_trans l l' l'' :
-    Permutation l l' -> Permutation l' l'' -> Permutation l l''.
-
-Local Hint Constructors Permutation.
-
-(** Some facts about [Permutation] *)
-
-Theorem Permutation_nil : forall (l : list A), Permutation [] l -> l = [].
-Proof.
-  intros l HF.
-  remember (@nil A) as m in HF.
-  induction HF; discriminate || auto.
-Qed.
-
-Theorem Permutation_nil_cons : forall (l : list A) (x : A),
- ~ Permutation nil (x::l).
-Proof.
-  intros l x HF.
-  apply Permutation_nil in HF; discriminate.
-Qed.
-
-(** Permutation over lists is a equivalence relation *)
-
-Theorem Permutation_refl : forall l : list A, Permutation l l.
-Proof.
-  induction l; constructor. exact IHl.
-Qed.
-
-Theorem Permutation_sym : forall l l' : list A,
- Permutation l l' -> Permutation l' l.
-Proof.
-  intros l l' Hperm; induction Hperm; auto.
-  apply perm_trans with (l':=l'); assumption.
-Qed.
-
-Theorem Permutation_trans : forall l l' l'' : list A,
- Permutation l l' -> Permutation l' l'' -> Permutation l l''.
-Proof.
-  exact perm_trans.
-Qed.
-
-End Permutation.
-
-Hint Resolve Permutation_refl perm_nil perm_skip.
-
-(* These hints do not reduce the size of the problem to solve and they
-   must be used with care to avoid combinatoric explosions *)
-
-Local Hint Resolve perm_swap perm_trans.
-Local Hint Resolve Permutation_sym Permutation_trans.
-
-(* This provides reflexivity, symmetry and transitivity and rewriting
-   on morphims to come *)
-
-Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := {
-  Equivalence_Reflexive := @Permutation_refl A ;
-  Equivalence_Symmetric := @Permutation_sym A ;
-  Equivalence_Transitive := @Permutation_trans A }.
-
-Instance Permutation_cons A :
- Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A) | 10.
-Proof.
-  repeat intro; subst; auto using perm_skip.
-Qed.
-
-Section Permutation_properties.
-
-Variable A:Type.
-
-Implicit Types a b : A.
-Implicit Types l m : list A.
-
-(** Compatibility with others operations on lists *)
-
-Theorem Permutation_in : forall (l l' : list A) (x : A),
- Permutation l l' -> In x l -> In x l'.
-Proof.
-  intros l l' x Hperm; induction Hperm; simpl; tauto.
-Qed.
-
-Global Instance Permutation_in' :
- Proper (Logic.eq ==> @Permutation A ==> iff) (@In A) | 10.
-Proof.
-  repeat red; intros; subst; eauto using Permutation_in.
-Qed.
-
-Lemma Permutation_app_tail : forall (l l' tl : list A),
- Permutation l l' -> Permutation (l++tl) (l'++tl).
-Proof.
-  intros l l' tl Hperm; induction Hperm as [|x l l'|x y l|l l' l'']; simpl; auto.
-  eapply Permutation_trans with (l':=l'++tl); trivial.
-Qed.
-
-Lemma Permutation_app_head : forall (l tl tl' : list A),
- Permutation tl tl' -> Permutation (l++tl) (l++tl').
-Proof.
-  intros l tl tl' Hperm; induction l;
-   [trivial | repeat rewrite <- app_comm_cons; constructor; assumption].
-Qed.
-
-Theorem Permutation_app : forall (l m l' m' : list A),
- Permutation l l' -> Permutation m m' -> Permutation (l++m) (l'++m').
-Proof.
-  intros l m l' m' Hpermll' Hpermmm';
-   induction Hpermll' as [|x l l'|x y l|l l' l''];
-    repeat rewrite <- app_comm_cons; auto.
-  apply Permutation_trans with (l' := (x :: y :: l ++ m));
-   [idtac | repeat rewrite app_comm_cons; apply Permutation_app_head]; trivial.
-  apply Permutation_trans with (l' := (l' ++ m')); try assumption.
-  apply Permutation_app_tail; assumption.
-Qed.
-
-Global Instance Permutation_app' :
- Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A) | 10.
-Proof.
-  repeat intro; now apply Permutation_app.
-Qed.
-
-Lemma Permutation_add_inside : forall a (l l' tl tl' : list A),
-  Permutation l l' -> Permutation tl tl' ->
-  Permutation (l ++ a :: tl) (l' ++ a :: tl').
-Proof.
-  intros; apply Permutation_app; auto.
-Qed.
-
-Lemma Permutation_cons_append : forall (l : list A) x,
-  Permutation (x :: l) (l ++ x :: nil).
-Proof. induction l; intros; auto. simpl. rewrite <- IHl; auto. Qed.
-Local Hint Resolve Permutation_cons_append.
-
-Theorem Permutation_app_comm : forall (l l' : list A),
-  Permutation (l ++ l') (l' ++ l).
-Proof.
-  induction l as [|x l]; simpl; intro l'.
-  rewrite app_nil_r; trivial. rewrite IHl.
-  rewrite app_comm_cons, Permutation_cons_append.
-  now rewrite <- app_assoc.
-Qed.
-Local Hint Resolve Permutation_app_comm.
-
-Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
-  Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
-Proof.
-  intros l l1 l2 a H. rewrite H.
-  rewrite app_comm_cons, Permutation_cons_append.
-  now rewrite <- app_assoc.
-Qed.
-Local Hint Resolve Permutation_cons_app.
-
-Theorem Permutation_middle : forall (l1 l2:list A) a,
-  Permutation (a :: l1 ++ l2) (l1 ++ a :: l2).
-Proof.
-  auto.
-Qed.
-Local Hint Resolve Permutation_middle.
-
-Theorem Permutation_rev : forall (l : list A), Permutation l (rev l).
-Proof.
-  induction l as [| x l]; simpl; trivial. now rewrite IHl at 1.
-Qed.
-
-Global Instance Permutation_rev' :
- Proper (@Permutation A ==> @Permutation A) (@rev A) | 10.
-Proof.
-  repeat intro; now rewrite <- 2 Permutation_rev.
-Qed.
-
-Theorem Permutation_length : forall (l l' : list A),
- Permutation l l' -> length l = length l'.
-Proof.
-  intros l l' Hperm; induction Hperm; simpl; auto. now transitivity (length l').
-Qed.
-
-Global Instance Permutation_length' :
- Proper (@Permutation A ==> Logic.eq) (@length A) | 10.
-Proof.
-  exact Permutation_length.
-Qed.
-
-Theorem Permutation_ind_bis :
- forall P : list A -> list A -> Prop,
-   P [] [] ->
-   (forall x l l', Permutation l l' -> P l l' -> P (x :: l) (x :: l')) ->
-   (forall x y l l', Permutation l l' -> P l l' -> P (y :: x :: l) (x :: y :: l')) ->
-   (forall l l' l'', Permutation l l' -> P l l' -> Permutation l' l'' -> P l' l'' -> P l l'') ->
-   forall l l', Permutation l l' -> P l l'.
-Proof.
-  intros P Hnil Hskip Hswap Htrans.
-  induction 1; auto.
-  apply Htrans with (x::y::l); auto.
-  apply Hswap; auto.
-  induction l; auto.
-  apply Hskip; auto.
-  apply Hskip; auto.
-  induction l; auto.
-  eauto.
-Qed.
-
-Ltac break_list l x l' H :=
-  destruct l as [|x l']; simpl in *;
-  injection H; intros; subst; clear H.
-
-Theorem Permutation_nil_app_cons : forall (l l' : list A) (x : A),
- ~ Permutation nil (l++x::l').
-Proof.
-  intros l l' x HF.
-  apply Permutation_nil in HF. destruct l; discriminate.
-Qed.
-
-Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a,
-  Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4).
-Proof.
-  intros l1 l2 l3 l4 a; revert l1 l2 l3 l4.
-  set (P l l' :=
-       forall l1 l2 l3 l4, l=l1++a::l2 -> l'=l3++a::l4 ->
-       Permutation (l1++l2) (l3++l4)).
-  cut (forall l l', Permutation l l' -> P l l').
-  intros H; intros; eapply H; eauto.
-  apply (Permutation_ind_bis P); unfold P; clear P.
-  - (* nil *)
-    intros; now destruct l1.
-  - (* skip *)
-    intros x l l' H IH; intros.
-    break_list l1 b l1' H0; break_list l3 c l3' H1.
-    auto.
-    now rewrite H.
-    now rewrite <- H.
-    now rewrite (IH _ _ _ _ eq_refl eq_refl).
-  - (* swap *)
-    intros x y l l' Hp IH; intros.
-    break_list l1 b l1' H; break_list l3 c l3' H0.
-    auto.
-    break_list l3' b l3'' H.
-    auto.
-    constructor. now rewrite Permutation_middle.
-    break_list l1' c l1'' H1.
-    auto.
-    constructor. now rewrite Permutation_middle.
-    break_list l3' d l3'' H; break_list l1' e l1'' H1.
-    auto.
-    rewrite perm_swap. constructor. now rewrite Permutation_middle.
-    rewrite perm_swap. constructor. now rewrite Permutation_middle.
-    now rewrite perm_swap, (IH _ _ _ _ eq_refl eq_refl).
-  - (*trans*)
-    intros.
-    destruct (In_split a l') as (l'1,(l'2,H6)).
-    rewrite <- H.
-    subst l.
-    apply in_or_app; right; red; auto.
-    apply perm_trans with (l'1++l'2).
-    apply (H0 _ _ _ _ H3 H6).
-    apply (H2 _ _ _ _ H6 H4).
-Qed.
-
-Theorem Permutation_cons_inv l l' a :
- Permutation (a::l) (a::l') -> Permutation l l'.
-Proof.
-  intro H; exact (Permutation_app_inv [] l [] l' a H).
-Qed.
-
-Theorem Permutation_cons_app_inv l l1 l2 a :
- Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2).
-Proof.
-  intro H; exact (Permutation_app_inv [] l l1 l2 a H).
-Qed.
-
-Theorem Permutation_app_inv_l : forall l l1 l2,
- Permutation (l ++ l1) (l ++ l2) -> Permutation l1 l2.
-Proof.
-  induction l; simpl; auto.
-  intros.
-  apply IHl.
-  apply Permutation_cons_inv with a; auto.
-Qed.
-
-Theorem Permutation_app_inv_r : forall l l1 l2,
- Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2.
-Proof.
-  induction l.
-  intros l1 l2; do 2 rewrite app_nil_r; auto.
-  intros.
-  apply IHl.
-  apply Permutation_app_inv with a; auto.
-Qed.
-
-Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a].
-Proof.
-  intros a l H; remember [a] as m in H.
-  induction H; try (injection Heqm as -> ->; clear Heqm);
-    discriminate || auto.
-  apply Permutation_nil in H as ->; trivial.
-Qed.
-
-Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b.
-Proof.
-  intros a b H.
-  apply Permutation_length_1_inv in H; injection H as ->; trivial.
-Qed.
-
-Lemma Permutation_length_2_inv :
-  forall a1 a2 l, Permutation [a1;a2] l -> l = [a1;a2] \/ l = [a2;a1].
-Proof.
-  intros a1 a2 l H; remember [a1;a2] as m in H.
-  revert a1 a2 Heqm.
-  induction H; intros; try (injection Heqm; intros; subst; clear Heqm);
-    discriminate || (try tauto).
-  apply Permutation_length_1_inv in H as ->; left; auto.
-  apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as ();
-    auto.
-Qed.
-
-Lemma Permutation_length_2 :
-  forall a1 a2 b1 b2, Permutation [a1;a2] [b1;b2] ->
-    a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1.
-Proof.
-  intros a1 b1 a2 b2 H.
-  apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto.
-Qed.
-
-Let in_middle l l1 l2 (a:A) : l = l1 ++ a :: l2 ->
- forall x, In x l <-> a = x \/ In x (l1++l2).
-Proof.
- intros; subst; rewrite !in_app_iff; simpl. tauto.
-Qed.
-
-Lemma NoDup_cardinal_incl (l l' : list A) : NoDup l -> NoDup l' ->
-  length l = length l' -> incl l l' -> incl l' l.
-Proof.
- intros N. revert l'. induction N as [|a l Hal Hl IH].
- - destruct l'; now auto.
- - intros l' Hl' E H x Hx.
-   assert (Ha : In a l') by (apply H; simpl; auto).
-   destruct (in_split _ _ Ha) as (l1 & l2 & H12). clear Ha.
-   rewrite in_middle in Hx; eauto.
-   destruct Hx as [Hx|Hx]; [left|right]; auto.
-   apply (IH (l1++l2)); auto.
-   * apply NoDup_remove_1 with a; rewrite <- H12; auto.
-   * apply eq_add_S.
-     simpl in E; rewrite E, H12, !app_length; simpl; auto with arith.
-   * intros y Hy. assert (Hy' : In y l') by (apply H; simpl; auto).
-     rewrite in_middle in Hy'; eauto.
-     destruct Hy'; auto. subst y; intuition.
-Qed.
-
-Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' ->
-  (forall x:A, In x l <-> In x l') -> Permutation l l'.
-Proof.
- intros N. revert l'. induction N as [|a l Hal Hl IH].
- - destruct l'; simpl; auto.
-   intros Hl' H. exfalso. rewrite (H a); auto.
- - intros l' Hl' H.
-   assert (Ha : In a l') by (apply H; simpl; auto).
-   destruct (In_split _ _ Ha) as (l1 & l2 & H12).
-   rewrite H12.
-   apply Permutation_cons_app.
-   apply IH; auto.
-   * apply NoDup_remove_1 with a; rewrite <- H12; auto.
-   * intro x. split; intros Hx.
-     + assert (Hx' : In x l') by (apply H; simpl; auto).
-       rewrite in_middle in Hx'; eauto.
-       destruct Hx'; auto. subst; intuition.
-     + assert (Hx' : In x l') by (rewrite (in_middle l1 l2 a); eauto).
-       rewrite <- H in Hx'. destruct Hx'; auto.
-       subst. destruct (NoDup_remove_2 _ _ _ Hl' Hx).
-Qed.
-
-Lemma NoDup_Permutation_bis l l' : NoDup l -> NoDup l' ->
-  length l = length l' -> incl l l' -> Permutation l l'.
-Proof.
- intros. apply NoDup_Permutation; auto.
- split; auto. apply NoDup_cardinal_incl; auto.
-Qed.
-
-Lemma Permutation_NoDup l l' : Permutation l l' -> NoDup l -> NoDup l'.
-Proof.
- induction 1; auto.
- * inversion_clear 1; constructor; eauto using Permutation_in.
- * inversion_clear 1 as [|? ? H1 H2]. inversion_clear H2; simpl in *.
-   constructor. simpl; intuition. constructor; intuition.
-Qed.
-
-Global Instance Permutation_NoDup' :
- Proper (@Permutation A ==> iff) (@NoDup A) | 10.
-Proof.
-  repeat red; eauto using Permutation_NoDup.
-Qed.
-
-End Permutation_properties.
-
-Section Permutation_map.
-
-Variable A B : Type.
-Variable f : A -> B.
-
-Lemma Permutation_map l l' :
-  Permutation l l' -> Permutation (map f l) (map f l').
-Proof.
- induction 1; simpl; eauto.
-Qed.
-
-Global Instance Permutation_map' :
-  Proper (@Permutation A ==> @Permutation B) (map f) | 10.
-Proof.
-  exact Permutation_map.
-Qed.
-
-End Permutation_map.
-
-Section Injection.
-
-Definition injective {A B} (f : A->B) :=
- forall x y, f x = f y -> x = y.
-
-Lemma injective_map_NoDup {A B} (f:A->B) (l:list A) :
- injective f -> NoDup l -> NoDup (map f l).
-Proof.
- intros Hf. induction 1 as [|x l Hx Hl IH]; simpl; constructor; trivial.
- rewrite in_map_iff. intros (y & Hy & Hy'). apply Hf in Hy. now subst.
-Qed.
-
-Lemma injective_bounded_surjective n f :
- injective f ->
- (forall x, x < n -> f x < n) ->
- (forall y, y < n -> exists x, x < n /\ f x = y).
-Proof.
- intros Hf H.
- set (l := seq 0 n).
- assert (P : incl (map f l) l).
- { intros x. rewrite in_map_iff. intros (y & <- & Hy').
-   unfold l in *. rewrite in_seq in *. simpl in *.
-   destruct Hy' as (_,Hy'). auto with arith. }
- assert (P' : incl l (map f l)).
- { unfold l.
-   apply NoDup_cardinal_incl; auto using injective_map_NoDup, seq_NoDup.
-   now rewrite map_length. }
- intros x Hx.
- assert (Hx' : In x l) by (unfold l; rewrite in_seq; auto with arith).
- apply P' in Hx'.
- rewrite in_map_iff in Hx'. destruct Hx' as (y & Hy & Hy').
- exists y; split; auto. unfold l in *; rewrite in_seq in Hy'.
- destruct Hy'; auto with arith.
-Qed.
-
-Lemma nat_bijection_Permutation n f :
- injective f -> (forall x, x < n -> f x < n) ->
- let l := seq 0 n in Permutation (map f l) l.
-Proof.
- intros Hf BD.
- apply NoDup_Permutation_bis; auto using injective_map_NoDup, seq_NoDup.
- * now rewrite map_length.
- * intros x. rewrite in_map_iff. intros (y & <- & Hy').
-   rewrite in_seq in *. simpl in *.
-   destruct Hy' as (_,Hy'). auto with arith.
-Qed.
-
-End Injection.
-
-Section Permutation_alt.
-Variable A:Type.
-Implicit Type a : A.
-Implicit Type l : list A.
-
-(** Alternative characterization of permutation
-    via [nth_error] and [nth] *)
-
-Let adapt f n :=
- let m := f (S n) in if le_lt_dec m (f 0) then m else pred m.
-
-Let adapt_injective f : injective f -> injective (adapt f).
-Proof.
- unfold adapt. intros Hf x y EQ.
- destruct le_lt_dec as [LE|LT]; destruct le_lt_dec as [LE'|LT'].
- - now apply eq_add_S, Hf.
- - apply Lt.le_lt_or_eq in LE.
-   destruct LE as [LT|EQ']; [|now apply Hf in EQ'].
-   unfold lt in LT. rewrite EQ in LT.
-   rewrite <- (Lt.S_pred _ _ LT') in LT.
-   elim (Lt.lt_not_le _ _ LT' LT).
- - apply Lt.le_lt_or_eq in LE'.
-   destruct LE' as [LT'|EQ']; [|now apply Hf in EQ'].
-   unfold lt in LT'. rewrite <- EQ in LT'.
-   rewrite <- (Lt.S_pred _ _ LT) in LT'.
-   elim (Lt.lt_not_le _ _ LT LT').
- - apply eq_add_S, Hf.
-   now rewrite (Lt.S_pred _ _ LT), (Lt.S_pred _ _ LT'), EQ.
-Qed.
-
-Let adapt_ok a l1 l2 f : injective f -> length l1 = f 0 ->
- forall n, nth_error (l1++a::l2) (f (S n)) = nth_error (l1++l2) (adapt f n).
-Proof.
- unfold adapt. intros Hf E n.
- destruct le_lt_dec as [LE|LT].
- - apply Lt.le_lt_or_eq in LE.
-   destruct LE as [LT|EQ]; [|now apply Hf in EQ].
-   rewrite <- E in LT.
-   rewrite 2 nth_error_app1; auto.
- - rewrite (Lt.S_pred _ _ LT) at 1.
-   rewrite <- E, (Lt.S_pred _ _ LT) in LT.
-   rewrite 2 nth_error_app2; auto with arith.
-   rewrite <- Minus.minus_Sn_m; auto with arith.
-Qed.
-
-Lemma Permutation_nth_error l l' :
- Permutation l l' <->
-  (length l = length l' /\
-   exists f:nat->nat,
-    injective f /\ forall n, nth_error l' n = nth_error l (f n)).
-Proof.
- split.
- { intros P.
-   split; [now apply Permutation_length|].
-   induction P.
-   - exists (fun n => n).
-     split; try red; auto.
-   - destruct IHP as (f & Hf & Hf').
-     exists (fun n => match n with O => O | S n => S (f n) end).
-     split; try red.
-     * intros [|y] [|z]; simpl; now auto.
-     * intros [|n]; simpl; auto.
-   - exists (fun n => match n with 0 => 1 | 1 => 0 | n => n end).
-     split; try red.
-     * intros [|[|z]] [|[|t]]; simpl; now auto.
-     * intros [|[|n]]; simpl; auto.
-   - destruct IHP1 as (f & Hf & Hf').
-     destruct IHP2 as (g & Hg & Hg').
-     exists (fun n => f (g n)).
-     split; try red.
-     * auto.
-     * intros n. rewrite <- Hf'; auto. }
- { revert l. induction l'.
-   - intros [|l] (E & _); now auto.
-   - intros l (E & f & Hf & Hf').
-     simpl in E.
-     assert (Ha : nth_error l (f 0) = Some a)
-      by (symmetry; apply (Hf' 0)).
-     destruct (nth_error_split l (f 0) Ha) as (l1 & l2 & L12 & L1).
-     rewrite L12. rewrite <- Permutation_middle. constructor.
-     apply IHl'; split; [|exists (adapt f); split].
-     * revert E. rewrite L12, !app_length. simpl.
-       rewrite <- plus_n_Sm. now injection 1.
-     * now apply adapt_injective.
-     * intro n. rewrite <- (adapt_ok a), <- L12; auto.
-       apply (Hf' (S n)). }
-Qed.
-
-Lemma Permutation_nth_error_bis l l' :
- Permutation l l' <->
-  exists f:nat->nat,
-    injective f /\
-    (forall n, n < length l -> f n < length l) /\
-    (forall n, nth_error l' n = nth_error l (f n)).
-Proof.
- rewrite Permutation_nth_error; split.
- - intros (E & f & Hf & Hf').
-   exists f. do 2 (split; trivial).
-   intros n Hn.
-   destruct (Lt.le_or_lt (length l) (f n)) as [LE|LT]; trivial.
-   rewrite <- nth_error_None, <- Hf', nth_error_None, <- E in LE.
-   elim (Lt.lt_not_le _ _ Hn LE).
- - intros (f & Hf & Hf2 & Hf3); split; [|exists f; auto].
-   assert (H : length l' <= length l') by auto with arith.
-   rewrite <- nth_error_None, Hf3, nth_error_None in H.
-   destruct (Lt.le_or_lt (length l) (length l')) as [LE|LT];
-    [|apply Hf2 in LT; elim (Lt.lt_not_le _ _ LT H)].
-   apply Lt.le_lt_or_eq in LE. destruct LE as [LT|EQ]; trivial.
-   rewrite <- nth_error_Some, Hf3, nth_error_Some in LT.
-   destruct (injective_bounded_surjective Hf Hf2 LT) as (y & Hy & Hy').
-   apply Hf in Hy'. subst y. elim (Lt.lt_irrefl _ Hy).
-Qed.
-
-Lemma Permutation_nth l l' d :
- Permutation l l' <->
-  (let n := length l in
-   length l' = n /\
-   exists f:nat->nat,
-    (forall x, x < n -> f x < n) /\
-    (forall x y, x < n -> y < n -> f x = f y -> x = y) /\
-    (forall x, x < n -> nth x l' d = nth (f x) l d)).
-Proof.
- split.
- - intros H.
-   assert (E := Permutation_length H).
-   split; auto.
-   apply Permutation_nth_error_bis in H.
-   destruct H as (f & Hf & Hf2 & Hf3).
-   exists f. split; [|split]; auto.
-   intros n Hn. rewrite <- 2 nth_default_eq. unfold nth_default.
-    now rewrite Hf3.
- - intros (E & f & Hf1 & Hf2 & Hf3).
-   rewrite Permutation_nth_error.
-   split; auto.
-   exists (fun n => if le_lt_dec (length l) n then n else f n).
-   split.
-   * intros x y.
-     destruct le_lt_dec as [LE|LT];
-      destruct le_lt_dec as [LE'|LT']; auto.
-     + apply Hf1 in LT'. intros ->.
-       elim (Lt.lt_irrefl (f y)). eapply Lt.lt_le_trans; eauto.
-     + apply Hf1 in LT. intros <-.
-       elim (Lt.lt_irrefl (f x)). eapply Lt.lt_le_trans; eauto.
-   * intros n.
-     destruct le_lt_dec as [LE|LT].
-     + assert (LE' : length l' <= n) by (now rewrite E).
-       rewrite <- nth_error_None in LE, LE'. congruence.
-     + assert (LT' : n < length l') by (now rewrite E).
-       specialize (Hf3 n LT). rewrite <- 2 nth_default_eq in Hf3.
-       unfold nth_default in Hf3.
-       apply Hf1 in LT.
-       rewrite <- nth_error_Some in LT, LT'.
-       do 2 destruct nth_error; congruence.
-Qed.
-
-End Permutation_alt.
-
-(* begin hide *)
-Notation Permutation_app_swap := Permutation_app_comm (only parsing).
-(* end hide *)
diff --git a/samples/Coq/Sorting.v b/samples/Coq/Sorting.v
deleted file mode 100755
index edb10c63..00000000
--- a/samples/Coq/Sorting.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Require Export Sorted.
-Require Export Mergesort.
diff --git a/samples/Coq/interval_discr.v b/samples/Coq/interval_discr.v
deleted file mode 100644
index ed2c0e37..00000000
--- a/samples/Coq/interval_discr.v
+++ /dev/null
@@ -1,419 +0,0 @@
-(** Sketch of the proof of {p:nat|p<=n} = {p:nat|p<=m} -> n=m
-
-  - preliminary results on the irrelevance of boundedness proofs
-  - introduce the notion of finite cardinal |A|
-  - prove that |{p:nat|p<=n}| = n
-  - prove that |A| = n /\ |A| = m -> n = m if equality is decidable on A
-  - prove that equality is decidable on A
-  - conclude
-*)
-
-(** * Preliminary results on [nat] and [le] *)
-
-(** Proving axiom K on [nat] *)
-
-Require Import Eqdep_dec.
-Require Import Arith.
-
-Theorem eq_rect_eq_nat :
-  forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = eq_rect p Q x p h.
-Proof.
-intros.
-apply K_dec_set with (p := h).
-apply eq_nat_dec.
-reflexivity.
-Qed.
-
-(** Proving unicity of proofs of [(n<=m)%nat] *)
-
-Scheme le_ind' := Induction for le Sort Prop.
-
-Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q.
-Proof.
-induction p using le_ind'; intro q.
- replace (le_n n) with
-  (eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)).
- 2:reflexivity.
-  generalize (refl_equal n).
-    pattern n at 2 4 6 10, q; case q; [intro | intros m l e].
-     rewrite <- eq_rect_eq_nat; trivial.
-     contradiction (le_Sn_n m); rewrite <- e; assumption.
- replace (le_S n m p) with
-  (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))).
- 2:reflexivity.
-  generalize (refl_equal (S m)).
-    pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS].
-     contradiction (le_Sn_n m); rewrite Heq; assumption.
-     injection HeqS; intro Heq; generalize l HeqS.
-      rewrite <- Heq; intros; rewrite <- eq_rect_eq_nat.
-      rewrite (IHp l0); reflexivity.
-Qed.
-
-(** Proving irrelevance of boundedness proofs while building
-    elements of interval *)
-
-Lemma dep_pair_intro :
-  forall (n x y:nat) (Hx : x<=n) (Hy : y<=n), x=y ->
-    exist (fun x => x <= n) x Hx = exist (fun x => x <= n) y Hy.
-Proof.
-intros n x y Hx Hy Heq.
-generalize Hy.
-rewrite <- Heq.
-intros.
-rewrite (le_uniqueness_proof x n Hx Hy0).
-reflexivity.
-Qed.
-
-(** * Proving that {p:nat|p<=n} = {p:nat|p<=m} -> n=m *)
-
-(** Definition of having finite cardinality [n+1] for a set [A] *)
-
-Definition card (A:Set) n :=
-  exists f,
-    (forall x:A, f x <= n) /\
-    (forall x y:A, f x = f y -> x = y) /\
-    (forall m, m <= n -> exists x:A, f x = m).
-
-Require Import Arith.
-
-(** Showing that the interval [0;n] has cardinality [n+1] *)
-
-Theorem card_interval : forall n, card {x:nat|x<=n} n.
-Proof.
-intro n.
-exists (fun x:{x:nat|x<=n} => proj1_sig x).
-split.
-(* bounded *)
-intro x; apply (proj2_sig x).
-split.
-(* injectivity *)
-intros (p,Hp) (q,Hq).
-simpl.
-intro Hpq.
-apply dep_pair_intro; assumption.
-(* surjectivity *)
-intros m Hmn.
-exists (exist (fun x : nat => x <= n) m Hmn).
-reflexivity.
-Qed.
-
-(** Showing that equality on the interval [0;n] is decidable *)
-
-Lemma interval_dec :
-  forall n (x y : {m:nat|m<=n}), {x=y}+{x<>y}.
-Proof.
-intros n (p,Hp).
-induction p; intros ([|q],Hq).
-left.
-  apply dep_pair_intro.
-  reflexivity.
-right.
-  intro H; discriminate H.
-right.
-  intro H; discriminate H.
-assert (Hp' : p <= n).
-  apply le_Sn_le; assumption.
-assert (Hq' : q <= n).
-  apply le_Sn_le; assumption.
-destruct (IHp Hp' (exist (fun m => m <= n) q Hq'))
-  as [Heq|Hneq].
-left.
-  injection Heq; intro Heq'.
-  apply dep_pair_intro.
-  apply eq_S.
-  assumption.
-right.
-  intro HeqS.
-  injection HeqS; intro Heq.
-  apply Hneq.
-  apply dep_pair_intro.
-  assumption.
-Qed.
-
-(** Showing that the cardinality relation is functional on decidable sets *)
-
-Lemma card_inj_aux :
-  forall (A:Type) f g n,
-    (forall x:A, f x <= 0) ->
-    (forall x y:A, f x = f y -> x = y) ->
-    (forall m, m <= S n -> exists x:A, g x = m)
-     -> False.
-Proof.
-intros A f g n Hfbound Hfinj Hgsurj.
-destruct (Hgsurj (S n) (le_n _)) as (x,Hx).
-destruct (Hgsurj n (le_S _ _ (le_n _))) as (x',Hx').
-assert (Hfx : 0 = f x).
-apply le_n_O_eq.
-apply Hfbound.
-assert (Hfx' : 0 = f x').
-apply le_n_O_eq.
-apply Hfbound.
-assert (x=x').
-apply Hfinj.
-rewrite <- Hfx.
-rewrite <- Hfx'.
-reflexivity.
-rewrite H in Hx.
-rewrite Hx' in Hx.
-apply (n_Sn _ Hx).
-Qed.
-
-(** For [dec_restrict], we use a lemma on the negation of equality
-that requires proof-irrelevance. It should be possible to avoid this
-lemma by generalizing over a first-order definition of [x<>y], say
-[neq] such that [{x=y}+{neq x y}] and [~(x=y /\ neq x y)]; for such
-[neq], unicity of proofs could be proven *)
-
-  Require Import Classical.
-  Lemma neq_dep_intro :
-   forall (A:Set) (z x y:A) (p:x<>z) (q:y<>z), x=y ->
-      exist (fun x => x <> z) x p = exist (fun x => x <> z) y q.
-  Proof.
-  intros A z x y p q Heq.
-   generalize q; clear q; rewrite <- Heq; intro q.
-   rewrite (proof_irrelevance _ p q); reflexivity.
-  Qed.
-
-Lemma dec_restrict :
-  forall (A:Set),
-    (forall x y :A, {x=y}+{x<>y}) ->
-     forall z (x y :{a:A|a<>z}), {x=y}+{x<>y}.
-Proof.
-intros A Hdec z (x,Hx) (y,Hy).
-destruct (Hdec x y) as [Heq|Hneq].
-left; apply neq_dep_intro; assumption.
-right; intro Heq; injection Heq; exact Hneq.
-Qed.
-
-Lemma pred_inj : forall n m,
-  0 <> n -> 0 <> m -> pred m = pred n -> m = n.
-Proof.
-destruct n.
-intros m H; destruct H; reflexivity.
-destruct m.
-intros _ H; destruct H; reflexivity.
-simpl; intros _ _ H.
-rewrite H.
-reflexivity.
-Qed.
-
-Lemma le_neq_lt : forall n m, n <= m -> n<>m -> n < m.
-Proof.
-intros n m Hle Hneq.
-destruct (le_lt_eq_dec n m Hle).
-assumption.
-contradiction.
-Qed.
-
-Lemma inj_restrict :
-  forall (A:Set) (f:A->nat) x y z,
-    (forall x y : A, f x = f y -> x = y)
-    -> x <> z -> f y < f z -> f z <= f x
-    -> pred (f x) = f y
-    -> False.
-
-(* Search error sans le type de f !! *)
-Proof.
-intros A f x y z Hfinj Hneqx Hfy Hfx Heq.
-assert (f z <> f x).
-  apply sym_not_eq.
-  intro Heqf.
-  apply Hneqx.
-  apply Hfinj.
-  assumption.
-assert (f x = S (f y)).
-  assert (0 < f x).
-    apply le_lt_trans with (f z).
-    apply le_O_n.
-    apply le_neq_lt; assumption.
-  apply pred_inj.
-  apply O_S.
-  apply lt_O_neq; assumption.
-  exact Heq.
-assert (f z <= f y).
-destruct (le_lt_or_eq _ _ Hfx).
-  apply lt_n_Sm_le.
-  rewrite <- H0.
-  assumption.
-  contradiction Hneqx.
-  symmetry.
-  apply Hfinj.
-  assumption.
-contradiction (lt_not_le (f y) (f z)).
-Qed.
-
-Theorem card_inj : forall m n (A:Set),
-  (forall x y :A, {x=y}+{x<>y}) ->
-  card A m -> card A n -> m = n.
-Proof.
-induction m; destruct n;
-intros A Hdec
- (f,(Hfbound,(Hfinj,Hfsurj)))
- (g,(Hgbound,(Hginj,Hgsurj))).
-(* 0/0 *)
-reflexivity.
-(* 0/Sm *)
-destruct (card_inj_aux _ _ _ _ Hfbound Hfinj Hgsurj).
-(* Sn/0 *)
-destruct (card_inj_aux _ _ _ _ Hgbound Hginj Hfsurj).
-(* Sn/Sm *)
-destruct (Hgsurj (S n) (le_n _)) as (xSn,HSnx).
-rewrite IHm with (n:=n) (A := {x:A|x<>xSn}).
-reflexivity.
-(* decidability of eq on {x:A|x<>xSm} *)
-apply dec_restrict.
-assumption.
-(* cardinality of {x:A|x<>xSn} is m *)
-pose (f' := fun x' : {x:A|x<>xSn} =>
-    let (x,Hneq) := x' in
-    if le_lt_dec (f xSn) (f x)
-    then pred (f x)
-    else f x).
-exists f'.
-split.
-(* f' is bounded *)
-unfold f'.
-intros (x,_).
-destruct (le_lt_dec (f xSn) (f x)) as [Hle|Hge].
-change m with (pred (S m)).
-apply le_pred.
-apply Hfbound.
-apply le_S_n.
-apply le_trans with (f xSn).
-exact Hge.
-apply Hfbound.
-split.
-(* f' is injective *)
-unfold f'.
-intros (x,Hneqx) (y,Hneqy) Heqf'.
-destruct (le_lt_dec (f xSn) (f x)) as [Hlefx|Hgefx];
-destruct (le_lt_dec (f xSn) (f y)) as [Hlefy|Hgefy].
-(* f xSn <= f x et f xSn <= f y *)
-assert (Heq : x = y).
-  apply Hfinj.
-  assert (f xSn <> f y).
-    apply sym_not_eq.
-    intro Heqf.
-    apply Hneqy.
-    apply Hfinj.
-    assumption.
-  assert (0 < f y).
-    apply le_lt_trans with (f xSn).
-    apply le_O_n.
-    apply le_neq_lt; assumption.
-  assert (f xSn <> f x).
-    apply sym_not_eq.
-    intro Heqf.
-    apply Hneqx.
-    apply Hfinj.
-    assumption.
-  assert (0 < f x).
-    apply le_lt_trans with (f xSn).
-    apply le_O_n.
-    apply le_neq_lt; assumption.
-  apply pred_inj.
-  apply lt_O_neq; assumption.
-  apply lt_O_neq; assumption.
-  assumption.
-apply neq_dep_intro; assumption.
-(* f y < f xSn <= f x *)
-destruct (inj_restrict A f x y xSn); assumption.
-(* f x < f xSn <= f y *)
-symmetry in Heqf'.
-destruct (inj_restrict A f y x xSn); assumption.
-(* f x < f xSn et f y < f xSn *)
-assert (Heq : x=y).
-  apply Hfinj; assumption.
-apply neq_dep_intro; assumption.
-(* f' is surjective *)
-intros p Hlep.
-destruct (le_lt_dec (f xSn) p) as [Hle|Hlt].
-(* case f xSn <= p *)
-destruct (Hfsurj (S p) (le_n_S _ _ Hlep)) as (x,Hx).
-assert (Hneq : x <> xSn).
-  intro Heqx.
-  rewrite Heqx in Hx.
-  rewrite Hx in Hle.
-  apply le_Sn_n with p; assumption.
-exists (exist (fun a => a<>xSn) x Hneq).
-unfold f'.
-destruct (le_lt_dec (f xSn) (f x)) as [Hle'|Hlt'].
-rewrite Hx; reflexivity.
-rewrite Hx in Hlt'.
-contradiction (le_not_lt (f xSn) p).
-apply lt_trans with (S p).
-apply lt_n_Sn.
-assumption.
-(* case p < f xSn *)
-destruct (Hfsurj p (le_S _ _ Hlep)) as (x,Hx).
-assert (Hneq : x <> xSn).
-  intro Heqx.
-  rewrite Heqx in Hx.
-  rewrite Hx in Hlt.
-  apply (lt_irrefl p).
-  assumption.
-exists (exist (fun a => a<>xSn) x Hneq).
-unfold f'.
-destruct (le_lt_dec (f xSn) (f x)) as [Hle'|Hlt'].
-  rewrite Hx in Hle'.
-  contradiction (lt_irrefl p).
-  apply lt_le_trans with (f xSn); assumption.
-  assumption.
-(* cardinality of {x:A|x<>xSn} is n *)
-pose (g' := fun x' : {x:A|x<>xSn} =>
-   let (x,Hneq) := x' in
-   if Hdec x xSn then 0 else g x).
-exists g'.
-split.
-(* g is bounded *)
-unfold g'.
-intros (x,_).
-destruct (Hdec x xSn) as [_|Hneq].
-apply le_O_n.
-assert (Hle_gx:=Hgbound x).
-destruct (le_lt_or_eq _ _ Hle_gx).
-apply lt_n_Sm_le.
-assumption.
-contradiction Hneq.
-apply Hginj.
-rewrite HSnx.
-assumption.
-split.
-(* g is injective *)
-unfold g'.
-intros (x,Hneqx) (y,Hneqy) Heqg'.
-destruct (Hdec x xSn) as [Heqx|_].
-contradiction Hneqx.
-destruct (Hdec y xSn) as [Heqy|_].
-contradiction Hneqy.
-assert (Heq : x=y).
-  apply Hginj; assumption.
-apply neq_dep_intro; assumption.
-(* g is surjective *)
-intros p Hlep.
-destruct (Hgsurj p (le_S _ _ Hlep)) as (x,Hx).
-assert (Hneq : x<>xSn).
-  intro Heq.
-  rewrite Heq in Hx.
-  rewrite Hx in HSnx.
-  rewrite HSnx in Hlep.
-  contradiction (le_Sn_n _ Hlep).
-exists (exist (fun a => a<>xSn) x Hneq).
-simpl.
-destruct (Hdec x xSn) as [Heqx|_].
-contradiction Hneq.
-assumption.
-Qed.
-
-(** Conclusion *)
-
-Theorem interval_discr :
-  forall n m, {p:nat|p<=n} = {p:nat|p<=m} -> n=m.
-Proof.
-intros n m Heq.
-apply card_inj with (A := {p:nat|p<=n}).
-apply interval_dec.
-apply card_interval.
-rewrite Heq.
-apply card_interval.
-Qed.