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