proposition: Lemma wellFormedTermCorrect2 : forall n : nat, wellFormedTerm n <> 0 -> exists t : Term, codeTerm t = n.
proof: Proof. intro n; eapply proj1; apply wellFormedTermTermsCorrect2. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(Arith Lia) hydras.Ackermann(code folProp extEqualNat codeList) hydras(Compat815)