(42steps)
PrintForm
Definitions
formula
equality
Sections
ClassicalProps(jlc)
Doc
At:
discrete
Formula
1
4
1
1
1.
Q:
Formula
Prop
2.
x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
3.
x1:
{x:Formula| Q(x) }
4.
x2:
Formula
5.
Q(x2)
6.
y@0:
Formula
7.
x3:
Formula
8.
x4:
Formula
Dec(x1
x2 = x3
x4)
By:
Decide (x1 = x3)
Generated subgoals:
1
9.
x1 = x3
Dec(x1
x2 = x3
x4)
2
9.
x1 = x3
Dec(x1
x2 = x3
x4)
About:
(42steps)
PrintForm
Definitions
formula
equality
Sections
ClassicalProps(jlc)
Doc
Dec(x1
x2 = x3x4)
x1 = x3 Dec(x1x2 = x3x4)
Prop
x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
Dec(x1x2 = x3x4)
Dec(x1x2 = x3x4)x1 = x3 Dec(x1x2 = x3x4)
