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