proposition: Lemma codeArityLNNRIsCorrect2 : forall n : nat, codeArityLNNR n <> 0 -> exists r : Relations LNN, codeLNNRelation r = n.
proof: Proof. intros n H; destruct n. - exists LT_; reflexivity. - now destruct H. Qed.
imports: Coq(Arith List) hydras.Ackermann(fol primRec code)