proposition: Lemma notCon2wNotCon : forall T : System, Inconsistent LNN T -> wInconsistent T.
proof: Proof. intros T H; unfold wInconsistent; exists (equal Zero Zero). exists 0; split. - intros x H0; elim H0. - split. + apply H. + intros n; apply H. Qed.
imports: hydras.Ackermann(folProof folProp LNN) Coq(Arith List)