proposition: Lemma env_morph p e1 e2 : (forall x, e1 x = e2 x) -> p @ e1 = p @ e2.
proof: Proof. revert e1 e2. induction p as [|? ? IHp|? IHp1 ? ? IHp2]; simpl. - reflexivity. - intros e1 e2 EQ. apply IHp. intros. apply EQ. - intros e1 e2 EQ. f_equal; [f_equal|]. + now apply IHp1. + f_equal. apply EQ. + apply IHp2. intros; apply EQ. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory