Initializing kernel...

1. Formula = Type (NBGCompiler.Type):
Writing formula F = Set({x | x in x -> Bot}); defines a syntactically well-formed Type (even though it is mathematically false / uninhabited). Defining a formula never proves anything!

2. Proof = Term (NBGCompiler.Expr):
To prove F, you must construct a term e from kernel primitives whose inferred type equals F. For false MK/NBG formulas, the compiler deterministically rejects every candidate term.

compr(x. Phi, z) : Comprehension
fn (h : A) => e : Implication Intro
e1 e2 : Modus Ponens (Elim)
Lam (x : Sort) => e : Universal Intro
tapp(e, t) : Universal Elim (Set guard)
pack(w, e, Sigma) : Existential Intro (Set guard)
pair(a,b) / fst(e) / snd(e)
inl(e,B) / inr(e,A) / abort(e,A)
refl(t) / sym(e) / trans(e1,e2)
heredity(x,y) / dunaev_proj(A,B)