At:
discrete implies bool equality
1
1
1
2
1
2
1
1
1
1
2
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)
8.
y3: y = y 
False
9.
inr(y3) = y1(y)
10.
z: y = y
False
By:
Witness8 z
THEN
Trivial
Generated subgoals:
None
About:
