PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank valid or falsifiable 1 1 2 1 1 1
1. L: Sequent List
2. eqS: {Sequent=}
3. eqF: {Formula=}
4. sL.((s) = 0)
5. sL.(disjoint(eqF;s.H;s.C))

z:Sequent. z(eqS) L |= z
By: UnivCD
Generated subgoal:

16. z: Sequent
7. z(eqS) L
|= z

About:
allimpliesassertlistequalintapplynatural_number