PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank all vars 1 1
1. L: Sequent List
2. eqS: {Sequent=}
3. eqF: {Formula=}
4. sL.((s) = 0)
5. hyp: Formula List
6. concl: Formula List
7. < hyp,concl > (eqS) L
8. z: Formula
9. z(eqF) hyp

v:Var. z = v
By: Using [`T',Sequent;`eq',eqS;`P',(s. (s) = 0);`z', < hyp,concl > ] (FwdThru Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z)) [4])
Generated subgoal:

110. ( < hyp,concl > ) = 0
v:Var. z = v

About:
existsequalintapplynatural_numberpairlistassert