proposition: Lemma equal_2 : forall m (Hm:NoDupA m) m' (Hm':NoDupA m') cmp, equal cmp m m' = true -> Equivb cmp m m'.
proof: Proof. unfold Equivb, equal. intros. destruct (andb_prop _ _ H); clear H. generalize (submap_2 Hm Hm' H0). generalize (submap_2 Hm' Hm H1). firstorder. Qed.
imports: FMapInterface