PrintForm Definitions sequent satisfaction Sections ClassicalProps(jlc) Doc

At: decidable sequent satisfiable

S:Sequent, a:Assignment. Dec(a |= S)
By:
UnivCD
THEN
Unfold `sequent_satisfiable` 0
Generated subgoal:

11. S: Sequent
2. a: Assignment
Dec(FS.H.a | F FS.C.a |= F )

About:
allor