Nuprl - Pf discrete Formula with rank 1 4 1

1. x: Formula
2. x2: Formula
3. x3: Formula
4. y:Formula. Dec(x2 = y)
5. y:Formula. Dec(x3 = y)
6. y@0: Formula

Dec(x2x3 = y@0)

By: let Solver FalseCase THEN FormulaEquality -1 in FormulaCases -1 THENL [Solver;Solver;Solver;Id;Solver]

Generated subgoal:

1 7. x5: Formula
8. x6: Formula
Dec(x2x3 = x5x6)

About: