proposition: Lemma eq_1 : forall (m m' : t), Equivb cmp m m' -> eq m m'.
proof: Proof. intros m m'. rewrite eq_seq; unfold seq. rewrite Equivb_Equivb. rewrite P.Equivb_elements. auto using LO.eq_1. Qed.
imports: FunInd FMapInterface FMapList ZArith Int