PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank all vars 1 1 1 1 1 1 1 2 1 5
1. z: Formula
2. y1: Formula
3. y2: Formula

(y1)+(y2)+1 = 0 (v:Var. y1y2 = v)
By: GenConclOnAps
Generated subgoals:

None

About:
impliesequalintaddapplynatural_numberexists