proposition: Lemma subFormulaImp : forall (f1 f2 : fol.Formula L) (v : nat) (s : fol.Term L), substF (f1 -> f2)%fol v s = (substF f1 v s -> substF f2 v s)%fol.
proof: Proof. intros f1 f2 v s. unfold substF, substituteFormulaHelp in |- *. rewrite (Formula_depth_rec2_imp 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}). unfold substituteFormulaImp at 1 in |- *. - induction (Formula_depth_rec2 L (fun x : fol.Formula L => nat * fol.Term L -> {y : fol.Formula L | depth L y = depth L x}) (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 = depth L (equal t t0)}) (fun (a : nat) (b : fol.Term L) => exist (fun y : fol.Formula L => depth L y = depth L (equal t t0)) (equal (substT t a b) (substT t0 a b)) (refl_equal (depth L (equal t t0)))) 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 = depth L (atomic r t)}) (fun (a : nat) (b : fol.Term L) => exist (fun y : fol.Formula L => depth L y = depth L (atomic r t)) (atomic r (substTs (arityR L r) t a b)) (refl_equal (depth L (atomic r t)))) H) substituteFormulaImp substituteFormulaNot substituteFormulaForall f1 (v, s)). 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 = depth L (equal t t0)}) (fun (a : nat) (b : fol.Term L) => exist (fun y : fol.Formula L => depth L y = depth L (equal t t0)) (equal (substT t a b) (substT t0 a b)) (refl_equal (depth L (equal t t0)))) 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 = depth L (atomic r t)}) (fun (a : nat) (b : fol.Term L) => exist (fun y : fol.Formula L => depth L y = depth L (atomic r t)) (atomic r (substTs (arityR L r) t a b)) (refl_equal (depth L (atomic r t)))) H) substituteFormulaImp substituteFormulaNot substituteFormulaForall f2 (v, s)). reflexivity. - apply substituteFormulaImpNice. - apply substituteFormulaNotNice. - apply substituteFormulaForallNice. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)