proposition: Lemma equal_1 : forall m m' cmp, Equivb cmp m m' -> equal cmp m m' = true.
proof: Proof. unfold equal; intros (m,b) (m',b') cmp; rewrite Equivb_Equivb; intros; simpl in *; rewrite equal_Equivb; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int