Nuprl - Pf zero_rank_all

PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

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 z(eqF) concl

v:Var. z = v

By: Analyze -1

Generated subgoals:

1 9. z(eqF) hyp
v:Var. z = v

2 9. z(eqF) concl
v:Var. z = v

About:

1	9. `z(eqF) hyp` `v:Var. z = v`
2	9. `z(eqF) concl` `v:Var. z = v`