Nuprl - Pf discrete Formula with rank 1 1 1 1 2 1

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

At: discrete Formula with rank 1 1 1 1 2 1

1. x: Formula
2. x2: Var
3. y: Formula
4. x3: Var
5. x2 = x3

x2 = x3

By: FormulaEquality -1

Generated subgoals:

None

About:

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