proposition: Lemma LNN2LNT_freeVarTs (n : nat) (ts : fol.Terms LNN n): freeVarTs (LNN2LNT_terms n ts) = freeVarTs ts.
proof: Proof. induction ts as [| n t ts Hrects]. - reflexivity. - simpl; transitivity (freeVarT t ++ freeVarTs ts). + rewrite <- Hrects; rewrite <- LNN2LNT_freeVarT; reflexivity. + reflexivity. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)