proposition: Lemma codeArityLNNFIsCorrect2 : forall n : nat, codeArityLNTF n <> 0 -> exists f : Functions LNN, codeLNTFunction f = n.
proof: Proof. apply codeArityLNTFIsCorrect2. Qed.
imports: Coq(Arith List) hydras.Ackermann(fol primRec code)