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

At: discrete union 1 1 3 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

inl(x1) = inr(y1) T1+T2

By: Analyze 0

Generated subgoal:

17. inl(x1) = inr(y1) T1+T2
False

About:
decidableunioninlinruniverseequalfalseall

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