proposition: Remark substituteFormulaImpNice : forall (f g : 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 z3 z4 : nat * fol.Term L -> {y : fol.Formula L | depth L y = depth L g}, (forall q : nat * fol.Term L, z3 q = z4 q) -> forall q : nat * fol.Term L, substituteFormulaImp f z1 g z3 q = substituteFormulaImp f z2 g z4 q.
proof: Proof. intros f g z1 z2 H z3 z4 H0 q; unfold substituteFormulaImp in |- *. rewrite H, H0; reflexivity. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)