PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank all vars 1 2 1 1 1 1 1 2 1 3
1. z: Formula
2. x1: Formula
3. x2: Formula

(x1)+(x2)+1 = 0 (v:Var. x1x2 = v)
By: GenConclOnAps
Generated subgoals:

None

About:
impliesequalintaddapplynatural_numberexists