(5steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

At: decidable equal union 2
1. A: Type
2. B: Type
3. y1: B
4. x: A
5. a1,a2:A. a1 = a2 a1 = a2
6. b1,b2:B. b1 = b2 b1 = b2
inr(y1) = inl(x) A+B inr(y1) = inl(x) A+B
By: ObviousFrom [-1]
Generated subgoals:

None

About:
unioninlinruniverseequalorall

(5steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc