proposition: Remark substituteFormulaNotNice : forall (f : fol.Formula L) (z1 z2 : nat * fol.Term L -> {y : fol.Formula L | depth L y = depth L f}), (forall q : nat * fol.Term L, z1 q = z2 q) -> forall q : nat * fol.Term L, substituteFormulaNot f z1 q = substituteFormulaNot f z2 q.
proof: Proof. intros ? ? ? H ?; unfold substituteFormulaNot in |- *; now rewrite H. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)