proposition: Lemma subFormulaIfThenElse : forall (f1 f2 f3 : fol.Formula L) (v : nat) (s : fol.Term L), substF (ifThenElseH f1 f2 f3) v s = ifThenElseH (substF f1 v s) (substF f2 v s) (substF f3 v s).
proof: Proof. intros ? ? ? ? ?; unfold ifThenElseH. now rewrite subFormulaAnd, !subFormulaImp, subFormulaNot. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)