PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank all vars 1 1 1 1 1 1 1 2
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
10. M: Formula List
11. N: Formula List
12. hyp = (M @ (z.N))
13. (M)+(z)+(N)+(concl) = 0
14. (z) = 0

v:Var. z = v
By:
MoveToConcl -1
THEN
TryOnAllHyps Thin
Generated subgoal:

11. z: Formula
(z) = 0 (v:Var. z = v)

About:
existsequallistintapplynatural_number
assertpairconsaddimplies