proposition: Lemma map2_alt_equiv : forall m m', map2_alt m m' = map2 m m'.
proof: Proof. unfold map2_alt. induction m. - simpl; auto; intros. induction m'; try destruct a; simpl; auto. rewrite IHm'; auto. - induction m'; destruct a. + simpl; f_equal. clear IHm. induction m; try destruct a; simpl; auto. rewrite IHm; auto. + destruct a0. simpl. destruct (X.compare t0 t1); simpl; f_equal. * apply IHm. * apply IHm. * apply IHm'. Qed.
imports: FMapInterface