proposition: Lemma LNT2LNT_term (t : Term): LNN2LNT_term (LNT2LNN_term t) = t.
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms LNT n) => LNN2LNT_terms n (LNT2LNN_terms n ts) = ts); simpl in |- *. - reflexivity. - intros f t0 H. unfold LNNArityF. now rewrite H. - reflexivity. - intros n t0 H t1 H0. now rewrite H, H0. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)