PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank all vars 1 1 1 1 1 1 1 2 1 1
1. z: Formula
2. x: Var

0 = 0 (v:Var. x = v)
By: Analyze 0
Generated subgoal:

13. 0 = 0
v:Var. x = v

About:
impliesequalintnatural_numberexists