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

At: discrete Formula with rank 1 1 1
1. x: Formula
2. x2: Var
3. y: Formula

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

14. x3: Var
Dec(x2 = x3)

About:
decidableequal

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