full sequent assignment Sections ClassicalProps(jlc) Doc

Def Sequent == (Formula List)(Formula List)

Thm* S:Sequent, a:Full(S). a |= S a | S full_sequent_assignment_properties

Thm* S:Sequent. Full(S) Assignment full_sequent_assignment_inc

In prior sections: sequent sequent equality sequent rank sequent satisfaction sequent falsification sequent sat lemmas