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