proposition: Lemma codeFreeVarTermIsPR : isPR 1 codeFreeVarTerm.
proof: Proof. unfold codeFreeVarTerm; apply compose1_1IsPR. - apply codeFreeVarTermTermsIsPR. - apply cPairPi1IsPR. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(List Arith) hydras.Ackermann(ListExt) hydras(folProp code Compat815)