proposition: Fact PL22_morph : forall x y, morph22 (PL22 pX x y) = PL22 pY (morph22 x) (morph22 y).
proof: Proof. Proof using Hphi. destruct Hphi. do 2 intros (((?&?)&?)&?); apply M22_equal; auto. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)