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

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

Dec(x1 = x2)

By: FalseCase THEN Analyze -2

Generated subgoal:

1 5. x1 = x2
x1 = x2

About: