(25steps)
PrintForm
Definitions
discrete
jlc
Sections
Support(jlc)
Doc
At:
discrete
implies
bool
equality
1
1
1
2
1
2
1
1
1.
T:
Type
2.
g:
x,y:T
(x = y)+(
x = y)
3.
x:
T
4.
y:
T
5.
x = y
6.
y1:
y@0:T
(y = y@0)+(
y = y@0)
7.
y1 = g(y)
InjCase(g(y,y) ; true
; false
)
By:
Witness6 y
Generated subgoal:
1
8.
y2:
(y = y)+(
y = y)
9.
y2 = y1(y)
InjCase(g(y,y) ; true
; false
)
About:
(25steps)
PrintForm
Definitions
discrete
jlc
Sections
Support(jlc)
Doc
y = y)
InjCase(g(y,y) ; true
; false)
(x = y)+(x = y)
(y = y@0)+(y = y@0)
InjCase(g(y,y) ; true; false)
y = y) InjCase(g(y,y) ; true; false)
