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