proposition: Fact F5 : Canon_plus (S (S n)) alpha (E0_succ beta).
proof: Proof. destruct alpha, beta; cbn; now apply L2_6_2. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)