PrintForm Definitions sequent falsification Sections ClassicalProps(jlc) Doc

At: decidable sequent falsifiable 1
1. S: Sequent
2. a: Assignment

Dec(a | S)
By: Unfold `sequent_falsifiable` 0
Generated subgoal:

1 Dec(FS.H.a |= F & FS.C.a | F)

About:
and