proposition: Lemma subFormulaForall : forall (f : fol.Formula L) (x v : nat) (s : fol.Term L), let nv := newVar (v :: freeVarT s ++ freeVarF f) in substF (allH x, f)%fol v s = match eq_nat_dec x v with | left _ => forallH x f | right _ => match In_dec eq_nat_dec x (freeVarT s) with | right _ => (allH x, substF f v s)%fol | left _ => (allH nv, substF (substF f x (v# nv) ) v s)%fol end end.
proof: Proof. intros f x v s nv. unfold substF at 1 in |- *. unfold substituteFormulaHelp in |- *. rewrite (Formula_depth_rec2_forall L) with (Q := fun _ : fol.Formula L => (nat * fol.Term L)%type) (P := fun x : fol.Formula L => {y : fol.Formula L | depth L y = depth L x}). - simpl in |- *; induction (eq_nat_dec x v); simpl in |- *. + reflexivity. + induction (In_dec eq_nat_dec x (freeVarT s)); simpl in |- *. fold nv in |- *. unfold substF at 2 in |- *; unfold substituteFormulaHelp in |- *; simpl in |- *. * induction (Formula_depth_rec2 L (fun x0 : fol.Formula L => nat * fol.Term L -> {y : fol.Formula L | depth L y = depth L x0}) (fun (t t0 : fol.Term L) (H : nat * fol.Term L) => prod_rec (fun _ : nat * fol.Term L => {y : fol.Formula L | depth L y = 0}) (fun (a0 : nat) (b0 : fol.Term L) => exist (fun y : fol.Formula L => depth L y = 0) (equal (substT t a0 b0) (substT t0 a0 b0)) (refl_equal 0)) H) (fun (r : Relations L) (t : fol.Terms L (arityR L r)) (H : nat * fol.Term L) => prod_rec (fun _ : nat * fol.Term L => {y : fol.Formula L | depth L y = 0}) (fun (a0 : nat) (b0 : fol.Term L) => exist (fun y : fol.Formula L => depth L y = 0) (atomic r (substTs (arityR L r) t a0 b0)) (refl_equal 0)) H) substituteFormulaImp substituteFormulaNot substituteFormulaForall f (x, var nv)). unfold substF in |- *; unfold substituteFormulaHelp in |- *; simpl in |- *. induction (Formula_depth_rec2 L (fun x1 : fol.Formula L => nat * fol.Term L -> {y : fol.Formula L | depth L y = depth L x1}) (fun (t t0 : fol.Term L) (H : nat * fol.Term L) => prod_rec (fun _ : nat * fol.Term L => {y : fol.Formula L | depth L y = 0}) (fun (a0 : nat) (b0 : fol.Term L) => exist (fun y : fol.Formula L => depth L y = 0) (equal (substT t a0 b0) (substT t0 a0 b0)) (refl_equal 0)) H) (fun (r : Relations L) (t : fol.Terms L (arityR L r)) (H : nat * fol.Term L) => prod_rec (fun _ : nat * fol.Term L => {y : fol.Formula L | depth L y = 0}) (fun (a0 : nat) (b0 : fol.Term L) => exist (fun y : fol.Formula L => depth L y = 0) (atomic r (substTs (arityR L r) t a0 b0)) (refl_equal 0)) H) substituteFormulaImp substituteFormulaNot substituteFormulaForall x0 (v, s)). simpl in |- *; reflexivity. * unfold substF in |- *; unfold substituteFormulaHelp in |- *; simpl in |- *. induction (Formula_depth_rec2 L (fun x0 : fol.Formula L => nat * fol.Term L -> {y : fol.Formula L | depth L y = depth L x0}) (fun (t t0 : fol.Term L) (H : nat * fol.Term L) => prod_rec (fun _ : nat * fol.Term L => {y : fol.Formula L | depth L y = 0}) (fun (a : nat) (b1 : fol.Term L) => exist (fun y : fol.Formula L => depth L y = 0) (equal (substT t a b1) (substT t0 a b1)) (refl_equal 0)) H) (fun (r : Relations L) (t : fol.Terms L (arityR L r)) (H : nat * fol.Term L) => prod_rec (fun _ : nat * fol.Term L => {y : fol.Formula L | depth L y = 0}) (fun (a : nat) (b1 : fol.Term L) => exist (fun y : fol.Formula L => depth L y = 0) (atomic r (substTs (arityR L r) t a b1)) (refl_equal 0)) H) substituteFormulaImp substituteFormulaNot substituteFormulaForall f (v, s)). simpl in |- *; reflexivity. - apply substituteFormulaImpNice. - apply substituteFormulaNotNice. - apply substituteFormulaForallNice. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)