sequent falsification Sections ClassicalProps(jlc) Doc

Def a | S == FS.H.a |= F & FS.C.a | F

Thm* a:Assignment, S:Sequent. SqStable(a | S) sq_stable__sequent_falsifiable

Thm* S:Sequent, a:Assignment. Dec(a | S) decidable__sequent_falsifiable