proposition: Lemma codeArityLNNFIsCorrect1 : forall f : Functions LNN, codeArityLNTF (codeLNTFunction f) = S (arityF LNN f).
proof: Proof. apply codeArityLNTFIsCorrect1. Qed.
imports: Coq(Arith List) hydras.Ackermann(fol primRec code)