PrintForm Definitions sequent rank Sections ClassicalProps(jlc) Doc

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

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

13. u1: Formula
4. v1: Formula List
(v)+(u1)+(v1) = 0 (u) > 0 (u)+(v)+(u1)+(v1) = 0

About:
equalintaddapplynatural_number
listimpliesorand