PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

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