PrintForm Definitions sequent valid Sections ClassicalProps(jlc) Doc

At: sequent valid wf

S:Sequent. |= S Type
By:
UnivCD
THEN
Unfold `sequent_valid` 0
Generated subgoal:

11. S: Sequent
(a:Full(S). a |= S) Type

About:
allmemberuniverse