Nuprl - Pf discrete Formula with rank 1 5 1

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

Dec(y1y2 = y@0)

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

Generated subgoal:

1 7. y3: Formula
8. y4: Formula
Dec(y1y2 = y3y4)

About: