PrintForm Definitions sequent rank Sections ClassicalProps(jlc) Doc

At: not list exists rank gt 0 rank 0 2 1 1 1 1 1 1 1 1
1. u: Formula
2. v: Formula List
3. concl: Formula List
4. fv.((f) > 0) False (v)+0 = 0
5. ((u) > 0 fv.((f) > 0))
6. False
7. ((u) > 0 fv.((f) > 0)) (u) > 0 & fv.((f) > 0)
8. (u) > 0
9. fv.((f) > 0)
10. (v)+0 = 0

(u)+(v)+0 = 0
By:
OnHyps [-3;-1] MoveToConcl
THEN
TryOnAllHyps Thin
Generated subgoal:

1 (v)+0 = 0 (u) > 0 (u)+(v)+0 = 0

About:
equalintaddapplynatural_number
listimpliesfalseorand