proposition: Lemma eq_equal : forall m m', eq m m' <-> equal m m' = true.
proof: Proof. intros (l,Hl,Hd); induction l as [ |a l IHl]. - intros (l',Hl',Hd'); unfold eq; simpl. destruct l'; unfold equal; simpl; intuition. - intros (l',Hl',Hd'); unfold eq. destruct l' as [ |p l']. + destruct a; unfold equal; simpl; intuition. + destruct a as (x,e). destruct p as (x',e'). unfold equal; simpl. destruct (compare x x') as [Hlt|Heq|Hlt]; simpl; [intuition| |intuition]. split. * intros [H0 H1]. unfold cmp, compare2eqb at 1. case (compare e e'); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH); clear HH; simpl. inversion_clear Hl. inversion_clear Hl'. apply nodefault_tail in Hd. apply nodefault_tail in Hd'. destruct (IHl H Hd (Build_farray H2 Hd')). unfold equal, eq in H5; simpl in H5; auto. * { intro H. destruct (andb_prop _ _ H) as [H0 H1]; clear H. split. - generalize H0; unfold cmp, compare2eqb. case (compare e e'); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH); auto; intro; discriminate. - inversion_clear Hl. inversion_clear Hl'. apply nodefault_tail in Hd. apply nodefault_tail in Hd'. destruct (IHl H Hd (Build_farray H3 Hd')). unfold equal, eq in H6; simpl in H6; auto. } Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance