(42steps)
PrintForm
Definitions
formula
equality
Sections
ClassicalProps(jlc)
Doc
At:
discrete
Formula
1
1
1
1
1.
Q:
Formula
Prop
2.
x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
3.
x1:
Var
4.
y:
Formula
5.
x:
Var
Dec(
x1
=
x
)
By:
Decide (x1 = x)
Generated subgoals:
1
6.
x1 = x
Dec(
x1
=
x
)
2
6.
x1 = x
Dec(
x1
=
x
)
About:
(42steps)
PrintForm
Definitions
formula
equality
Sections
ClassicalProps(jlc)
Doc
Dec(
x1
= x)
x1 = x Dec(x1 = x)
Prop
x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
Dec(x1 = x)
Dec(x1 = x)x1 = x Dec(x1 = x)
