At:
discrete implies bool equality
1
1
1
1
1
1
1
1.
T: Type
2.
g: x:T
y:T. (x = y)+(
x = y)
3.
x: T
4.
y: T
5.
y1: y:T(x = y)+(x = y)
6.
y1 = g(x) 
(y:T. (x = y)+(x = y))
7.
y2: (x = y)+(x = y)
8.
y2 = y1(y)
InjCase(y2 ; true
; false) 
By:
Analyze 7
THEN
Reduce 0
Generated subgoals:
None
About:
