proposition: Lemma reduceIfThenElse (f1 f2 f3 f4 f5 f6 : Formula) (T : System): SysPrf T (iffH f1 f4) -> SysPrf T (iffH f2 f5) -> SysPrf T (iffH f3 f6) -> SysPrf T (iffH (ifThenElseH f1 f2 f3) (ifThenElseH f4 f5 f6)).
proof: Proof. intros; apply reduceAnd; apply reduceImp. - assumption. - assumption. - apply reduceNot; assumption. - assumption. Qed.
imports: Coq(Ensembles Lists.List Peano_dec) hydras.Ackermann(ListExt folProof folLogic folProp)