proposition: Lemma codeArityLNTFIsCorrect2 : forall n : nat, codeArityLNTF n <> 0 -> exists f : Functions LNT, codeLNTFunction f = n.
proof: Proof. intros n H; destruct n as [| n]. - exists Plus_; easy. - destruct n as [| n]. + exists Times_; easy. + destruct n as [| n]. * exists Succ_; easy. * destruct n as [| n]. -- exists Zero_; easy. -- destruct H; reflexivity. Qed.
imports: Coq(Arith List) hydras.Ackermann(fol primRec code)