Thms decidability Sections ClassicalProps(jlc) Doc

fvar Def F == inl(F)

Thm* x:Var. x Formula

About:
!abstractioninlallmember