proposition: Lemma eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3.
proof: Proof. intros m1 m2 M3; rewrite 3 eq_seq; unfold seq. intros; eapply LO.eq_trans; eauto. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia