fact: Definition wInconsistent (T : System) := exists f : Formula, (exists v : nat, (forall x : nat, In x (freeVarF f) -> v = x) /\ SysPrf T (existH v (notH f)) /\ (forall n : nat, SysPrf T (substF f v (natToTerm n)))).
imports: hydras.Ackermann(folProof folProp LNN) Coq(Arith List)