proposition: Fact MU22_morph : forall x y, morph22 (MU22 pX mX x y) = MU22 pY mY (morph22 x) (morph22 y).
proof: Proof. Proof using Hphi. destruct Hphi as [ G1 G2 G3 G4 G6 ]. do 2 intros (((?&?)&?)&?); apply M22_equal; repeat rewrite G3; repeat rewrite G4; auto. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)