proposition: Lemma eq_2 : forall m m', eq m m' -> MapS.Equivb cmp m m'.
proof: Proof. intros m m'. rewrite eq_seq; unfold seq. rewrite Equivb_Equivb. rewrite Equivb_elements. intros. generalize (LO.eq_2 H). auto. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia