proposition: Lemma equal_1 : forall m (Hm:NoDupA m) m' (Hm': NoDupA m') cmp, Equivb cmp m m' -> equal cmp m m' = true.
proof: Proof. unfold Equivb, equal. intuition. apply andb_true_intro; split; apply submap_1; unfold Submap; firstorder. Qed.
imports: FMapInterface