PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank valid or falsifiable 1 1 2 1 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))
6. z: Sequent
7. z(eqS) L

|= z
By: Using [`T',Sequent;`eq',eqS;`P',(s. disjoint(eqF;s.H;s.C));`L',L;`z',z] (FwdThru Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z)) [-3])
Generated subgoal:

18. disjoint(eqF;z.H;z.C)
|= z

About:
listequalintapplynatural_numberassert