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

At: discrete Formula with rank 1 1 1 1 2
1. x: Formula
2. x2: Var
3. y: Formula
4. x3: Var
5. x2 = x3

Dec(x2 = x3)
By:
FalseCase
THEN
Analyze -2
Generated subgoal:

15. x2 = x3
x2 = x3

About:
decidableequal

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