proposition: Lemma subFormulaId : forall (f : fol.Formula L) (v : nat), substF f v (var v) = f.
proof: Proof. intros f v. induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]. - now rewrite subFormulaEqual, !subTermId. - now rewrite subFormulaRelation, subTermsId. - now rewrite subFormulaImp, Hrecf1, Hrecf0. - now rewrite subFormulaNot, Hrecf. - rewrite subFormulaForall; destruct (eq_nat_dec n v) as [e|ne]. + reflexivity. + induction (In_dec eq_nat_dec n (freeVarT (var v))) as [a|b]. * elim ne; destruct a as [H| H]. -- now subst. -- destruct H. * now rewrite Hrecf. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)