proposition: Lemma codeLNTRelationInj : forall R S : LNTRelation, codeLNTRelation R = codeLNTRelation S -> R = S.
proof: Proof. intros R S H; destruct R; destruct S; reflexivity || discriminate H. Qed.
imports: Coq(Arith List) hydras.Ackermann(fol primRec code)