(27steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc

At: discrete union 1 1 4 2 1 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
8. y = y1

False
By:
UnfoldTopAb 6
THEN
FwdThru 6 [8]
THEN
Trivial
Generated subgoals:

None

About:
decidableunioninruniverseequalfalseall

(27steps) PrintForm Definitions discrete jlc Sections Support(jlc) Doc