(45steps)
PrintForm
Definitions
formula
equality
Sections
ClassicalProps(jlc)
Doc
At:
discrete
Formula
with
rank
1
1
1
1
1.
x:
Formula
2.
x2:
Var
3.
y:
Formula
4.
x3:
Var
Dec(
x2
=
x3
)
By:
Decide (x2 = x3)
Generated subgoals:
1
5.
x2 = x3
Dec(
x2
=
x3
)
2
5.
x2 = x3
Dec(
x2
=
x3
)
About:
(45steps)
PrintForm
Definitions
formula
equality
Sections
ClassicalProps(jlc)
Doc
Dec(
x2
= x3)
x2 = x3 Dec(x2 = x3)
Dec(x2 = x3)
Dec(x2 = x3)x2 = x3 Dec(x2 = x3)
