proposition: Lemma list_eq_spec : forall l1 l2, if list_eq l1 l2 then l1 = l2 else l1 <> l2.
proof: Proof. induction l1;destruct l2;simpl;intros;trivial;try (intro;discriminate;fail). generalize (Aeq_spec a a0);destruct (Aeq a a0);intros;subst;trivial. generalize (IHl1 l2);destruct (list_eq l1 l2);intros;subst;trivial. intro H1;injection H1;auto. intro H1;injection H1;auto. Qed.
imports: Coq(List)