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