proposition: Lemma LNN2LNT_freeVarT (t : fol.Term LNN): freeVarT (LNN2LNT_term t) = freeVarT t.
proof: Proof. induction t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms LNN n) => freeVarTs (LNN2LNT_terms n ts) = freeVarTs ts). - intros; reflexivity. - intros; simpl; repeat rewrite freeVarTApply; now apply IHt. - intros; simpl; reflexivity. - transitivity (freeVarT t ++ freeVarTs t0). + rewrite <- IHt0; rewrite <- IHt; reflexivity. + reflexivity. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)