At:
discrete union
1
1
2
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.
y: T2
6.
x1: T1
7.
inr(y) = inl(x1) 
T1+T2
False
By:
ApFunToHypEquands `z' InjCase[z]( 0 ; 1) 
7
THEN
Reduce -1
Generated subgoal:
| 1 | 8. 1 = 0
False |
About:
