proposition: Lemma nnE (T : System) (f : Formula): SysPrf T (~ ~ f)%fol -> SysPrf T f.
proof: Proof. intros H; apply impE with (~ ~ f)%fol. - apply impE with (~ f -> ~ ~ ~ f)%fol. + exists (nil (A:=Formula)). exists (CP L f (~ ~ f)%fol); contradiction. + apply impI. apply contradiction with (~ f)%fol. apply Axm. right; constructor. apply sysWeaken; assumption. - assumption. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)