proposition: Lemma equal_IfEq : forall (m1 m2:t elt), IfEq (equal cmp m1 m2) (elements m1) (elements m2).
proof: Proof. intros; unfold equal. rewrite <- (app_nil_r (elements m1)). replace (elements m2) with (flatten_e (cons m2 (End _))) by (rewrite cons_1; simpl; rewrite app_nil_r; auto). apply equal_cont_IfEq. intros. apply equal_end_IfEq; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int