fact: Definition substituteFormulaImp (f : fol.Formula L) (frec : nat * fol.Term L -> {y : fol.Formula L | depth L y = depth L f}) (g : fol.Formula L) (grec : nat * fol.Term L -> {y : fol.Formula L | depth L y = depth L g}) (p : nat * fol.Term L) : {y : fol.Formula L | depth L y = depth L (impH f g)} := match frec p with | exist f' prf1 => match grec p with | exist g' prf2 => exist (fun y : fol.Formula L => depth L y = S (Nat.max (depth L f) (depth L g))) (impH f' g') (eq_ind_r (fun n : nat => S (Nat.max n (depth L g')) = S (Nat.max (depth L f) (depth L g))) (eq_ind_r (fun n : nat => S (Nat.max (depth L f) n) = S (Nat.max (depth L f) (depth L g))) (refl_equal (S (Nat.max (depth L f) (depth L g)))) prf2) prf1) end end.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)