proposition: Lemma LNT2LNN_freeVarF (f : Formula): freeVarF (LNT2LNN_formula f) = freeVarF f.
proof: Proof. induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; simpl in |- *. - repeat rewrite LNT2LNN_freeVarT; reflexivity. - destruct r. - now rewrite Hrecf1, Hrecf0. - assumption. - now rewrite Hrecf. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)