Nuprl - Pf zero_rank_all_vars 1 1 1 1 1 1 1 2 1 1 1

PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: zero rank all vars 1 1 1 1 1 1 1 2 1 1 1

1. z: Formula
2. x: Var
3. 0 = 0

v:Var. x = v

By: With x (Analyze 0)

Generated subgoals:

None

About: