Thms decidability Sections ClassicalProps(jlc) Doc

Formula Def Formula == rec(formula.Var+formula+(formulaformula)+(formulaformula)+(formulaformula))

Thm* Formula Type

Var Def Var == Atom

Thm* Var Type

fvar Def F == inl(F)

Thm* x:Var. x Formula

About:
!abstractioninlallmemberatom
universerecunionproduct