At: zero rank all vars 1 2 1 1 1 1 1
1. L: Sequent List
2. eqS: {Sequent=
}
3. eqF: {Formula=}
4. 
s
L.(
(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
v:Var. z = 
v
By: Assert ((z) = 0)
Generated subgoals:| 1 | (z) = 0 |
| 2 | 14. (z) = 0
v:Var. z = v |
About:
