proposition: Remark RP : P alpha.
proof: Proof. split. apply R1. apply RB. apply RC. apply RD. apply RE. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)