fact: Definition substituteFormulaForall (n : nat) (f : fol.Formula L) (frec : forall b : fol.Formula L, lt_depth b (forallH n f) -> nat * fol.Term L -> {y : fol.Formula L | depth L y = depth L b}) (p : nat * fol.Term L) : {y : fol.Formula L | depth L y = depth L (forallH n f)} := match p with | (v, s) => match eq_nat_dec n v with | left _ => exist (fun y : fol.Formula L => depth L y = S (depth L f)) (forallH n f) (refl_equal (depth L (forallH n f))) | right _ => match In_dec eq_nat_dec n (freeVarT s) with | left _ => let nv := newVar (v :: freeVarT s ++ freeVarF f) in match frec f (depthForall L f n) (n, var nv) with | exist f' prf1 => match frec f' (eqDepth L f' f (forallH n f) (sym_eq prf1) (depthForall L f n)) p with | exist f'' prf2 => exist (fun y : fol.Formula L => depth L y = S (depth L f)) (forallH nv f'') (eq_ind_r (fun n : nat => S n = S (depth L f)) (refl_equal (S (depth L f))) (trans_eq prf2 prf1)) end end | right _ => match frec f (depthForall L f n) p with | exist f' prf1 => exist (fun y : fol.Formula L => depth L y = S (depth L f)) (forallH n f') (eq_ind_r (fun n : nat => S n = S (depth L f)) (refl_equal (S (depth L f))) prf1) end end end end.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)