proposition: Lemma opt_eq_spec : forall o1 o2, if opt_eq o1 o2 then o1 = o2 else o1 <> o2.
proof: Proof. intros [a1|] [a2|];simpl;trivial;try (intro H;discriminate H;fail). generalize (Aeq_spec a1 a2);destruct (Aeq a1 a2);intros;subst;trivial. intro H1;injection H1;auto. Qed.
imports: Coq(List)