At:
discrete union
1
1
4
2
1
1
1.
T1: Type{i}
2.
T2: Type{j}
3.
x,y:T1. Dec(x = y)
4.
y: T2
5.
y1: T2
6.
y = y1
7.
inr(y) = inr(y1) 
T1+T2
False
By:
ApFunToHypEquands `z' InjCase[z]( y1 ; z) T2 7
THEN
Reduce -1
Generated subgoal:
| 1 | 8. y = y1
False |
About:
