Nuprl - Pf discrete Formula with rank 1 1

(45steps) PrintForm Definitions formula equality Sections ClassicalProps(jlc) Doc

At: discrete Formula with rank 1 1

1. x: Formula
2. x2: Var

y:Formula. Dec(x2 = y)

By: Analyze 0

Generated subgoal:

1 3. y: Formula
Dec(x2 = y)

About:

(45steps) PrintForm Definitions formula equality Sections ClassicalProps(jlc) Doc