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