proposition: Lemma Equiv_Equivb : forall m m', Equiv m m' <-> Equivb m m'.
proof: Proof. unfold Equiv, Equivb, Raw.Equivb, cmp; intuition; specialize (H1 k e e' H H2). - unfold compare2eqb; destruct (compare e e'); auto; apply lt_not_eq in l; auto. - unfold compare2eqb in *; destruct (compare e e'); auto; inversion H1. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance