proposition: Lemma LNT2LNN_freeVarT ( t : Term): freeVarT (LNT2LNN_term t) = freeVarT t.
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms LNT n) => freeVarTs (LNT2LNN_terms n ts) = freeVarTs ts); simpl in |- *. - reflexivity. - intros f t0 H; transitivity (freeVarTs (LNT2LNN_terms (LNTFunctionArity f) t0)). + reflexivity. + now rewrite H. - reflexivity. - intros n t0 H t1 H0; transitivity (freeVarT (LNT2LNN_term t0) ++ freeVarTs (LNT2LNN_terms n t1)). + reflexivity. + 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)