proposition: Lemma eqListSym : forall l l', eqList l l' -> eqList l' l.
proof: Proof. intro l; induction l. intro l'; induction l'; auto. intro l'; induction l'; auto. simpl. intro H. destruct H as [Haa0 Hll']. split; intuition. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms