proposition: Lemma Mphi_morph M e1 e2 : (forall x, e1 x = e2 x) -> M @@ e1 = M @@ e2.
proof: Proof. revert e1 e2; induction M as [|? ? IHM|? ? IHM]; simpl; intros e1 e2 EQ; trivial. - apply IHM. intros; apply EQ. - f_equal. * apply IHM. intros; apply EQ. * f_equal. apply EQ. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory