proposition: Lemma wellFormedTermsCorrect2 : forall n : nat, wellFormedTerms n <> 0 -> exists m : nat, (exists ts : Terms m, codeTerms ts = n).
proof: Proof. intro n; eapply proj2; apply wellFormedTermTermsCorrect2. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(Arith Lia) hydras.Ackermann(code folProp extEqualNat codeList) hydras(Compat815)