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

At: discrete Formula with rank 1 2 1
1. x: Formula
2. x1: Formula
3. y:Formula. Dec(x1 = y)
4. y@0: Formula

Dec(x1 = y@0)
By: let Solver FalseCase THEN FormulaEquality -1 in FormulaCases -1 THENL [Solver;Id;Solver;Solver;Solver]
Generated subgoal:

15. x2: Formula
Dec(x1 = x2)

About:
decidableequalall

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