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

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

None

About:
unioninruniverseequalorall

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