proposition: Lemma LNT2LNN_subFormula : forall (f : Formula) (v : nat) (s : Term), LNT2LNN_formula (substF f v s) = substF (LNT2LNN_formula f) v (LNT2LNN_term s).
proof: Proof. intro f. elim f using Formula_depth_ind2; simpl in |- *. - intros t t0 v s; now repeat rewrite LNT2LNN_subTerm. - intro r; destruct r. - intros f0 H f1 H0 v s; rewrite (subFormulaImp LNT). simpl; now rewrite H, H0, (subFormulaImp LNN). - intros f0 H n H0; rewrite (subFormulaNot LNT); simpl. now rewrite H, (subFormulaNot LNN). - intros v a H v0 s; rewrite (subFormulaForall LNT), (subFormulaForall LNN). destruct (eq_nat_dec v v0) as [e | n]. + reflexivity. + rewrite LNT2LNN_freeVarT. destruct (In_dec eq_nat_dec v (freeVarT s)) as [i | i]. * simpl; repeat rewrite H; simpl. -- now rewrite LNT2LNN_freeVarF. -- apply depthForall. -- eapply eqDepth. ++ symmetry; rewrite subFormulaDepth; symmetry. reflexivity. ++ apply depthForall. * simpl; rewrite H. -- reflexivity. -- apply depthForall. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)