proposition: Lemma eqListRefl : forall l, eqList l l.
proof: Proof. intro l; induction l; simpl. trivial. split; try assumption. reflexivity. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms