proposition: Lemma codeSubTermsIsPR : isPR 3 codeSubTerms.
proof: Proof. unfold codeSubTerms; apply compose3_1IsPR. - apply codeSubTermTermsIsPR. - apply cPairPi2IsPR. Qed.
imports: hydras.Ackermann(primRec cPair folProp code extEqualNat) Coq(Arith) hydras(Compat815) NewNotations