proposition: Lemma eq_equal : forall m m', eq m m' <-> equal m m' = true.
proof: Proof. intros (l,Hl,d,Hd); induction l. intros (l',Hl',d',Hd'); unfold eq, equal; simpl; case (eq_dec d d'); intro; destruct l'; simpl; intuition. intros (l',Hl',d',Hd'); unfold eq. simpl. unfold equal; simpl; case (eq_dec d d'); intro He; simpl; [ | now intuition]. destruct 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. unfold cmp at 1. case (compare e e'); subst x' e'; 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_slist H2 Hd')). unfold equal, eq in H5, H4; simpl in H5, H4; subst d'. destruct (eq_dec d d); auto. destruct (andb_prop _ _ H); clear H. generalize H0; unfold cmp. case (compare e e'); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH); auto; intro; discriminate. destruct (andb_prop _ _ H); clear H. inversion_clear Hl. inversion_clear Hl'. apply nodefault_tail in Hd. apply nodefault_tail in Hd'. destruct (IHl H Hd (Build_slist H3 Hd')). unfold equal, eq in H5, H6; simpl in H5, H6; subst d'. destruct (eq_dec d d); auto. now contradict n. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance