PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

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

sL.|= s (a:Assignment. sL.a | s)
By: FwdThru Thm* P:(TProp), L:T List. xL.P(x) xL.(P(x)) [-1]
Generated subgoal:

16. sL.(disjoint(eqF;s.H;s.C))
sL.|= s (a:Assignment. sL.a | s)

About:
orexistslistequalintapplynatural_number