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

1. x: Formula
2. x1: Formula
3. y@0: Formula
4. x2: Formula
5. x1 = x2

Dec(x1 = x2)

By: TrueCase THEN FormulaEquality 0 THEN Trivial

Generated subgoals:

None

About: