proposition: Lemma subFormulaDepth : forall (f : fol.Formula L) (v : nat) (s : fol.Term L), depth L (substF f v s) = depth L f.
proof: Proof. intros f v s; unfold substF in |- *. induction (substituteFormulaHelp f v s) as [x p]; now simpl. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)