proposition: Lemma Equivb_Equivb : forall cmp m m', Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'.
proof: Proof. intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In. intuition. - generalize (H0 k); do 2 rewrite In_alt; intuition. - generalize (H0 k); do 2 rewrite In_alt; intuition. - generalize (H0 k); do 2 rewrite <- In_alt; intuition. - generalize (H0 k); do 2 rewrite <- In_alt; intuition. Qed.
imports: FunInd FMapInterface FMapList ZArith Int