proposition: Lemma PNSubst_ok n P1 M1 P2 l P3 : PNSubst P1 M1 P2 n = Some P3 -> M1@@l == P2@l -> P1@l == P3@l.
proof: Proof. unfold PNSubst. assert (H := POneSubst_ok P1 M1 P2); destruct POneSubst; try discriminate. destruct n; inversion_clear 1. intros. rewrite <- PNSubst1_ok; auto. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory