proposition: Lemma codeLNTFunctionInj : forall f g : LNTFunction, codeLNTFunction f = codeLNTFunction g -> f = g.
proof: Proof. intros f g H; destruct f; destruct g; reflexivity || discriminate H. Qed.
imports: Coq(Arith List) hydras.Ackermann(fol primRec code)