proposition: Lemma reduceNot (f1 f2 : Formula) (T : System): SysPrf T (iffH f1 f2) -> SysPrf T (iffH (notH f1) (notH f2)).
proof: Proof. assert (H: forall (f1 f2 : Formula) (T : System), SysPrf T (iffH f1 f2) -> SysPrf T (impH (notH f1) (notH f2))) by (intros f0 f3 T0 H; apply (cp2 L), (iffE2 L), H). intros H0; apply (iffI L). - now apply H. - apply H; now apply (iffSym L). Qed.
imports: Coq(Ensembles Lists.List Peano_dec) hydras.Ackermann(ListExt folProof folLogic folProp)