proposition: Lemma PNSubstL_ok m n LM1 P1 l : MPcond LM1 l -> P1@l == (PNSubstL P1 LM1 m n)@l.
proof: Proof. revert LM1 P1. induction m as [|m IHm]; simpl; intros LM1 P2 H; assert (H' := PSubstL_ok n LM1 P2); destruct PSubstL; auto; try reflexivity. rewrite <- IHm; auto. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory