proposition: Lemma PSubstL_ok n LM1 P1 P2 l : PSubstL P1 LM1 n = Some P2 -> MPcond LM1 l -> P1@l == P2@l.
proof: Proof. revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros P3 H **. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition. * now apply IH. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory