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