proposition: Lemma subFormulaIff : forall (f1 f2 : fol.Formula L) (v : nat) (s : fol.Term L), substF (iffH f1 f2) v s = iffH (substF f1 v s) (substF f2 v s).
proof: Proof. intros ? ? v s; unfold iffH in |- *. rewrite subFormulaAnd; now repeat rewrite subFormulaImp. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)