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

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

None

About:
unioninlinruniverseequalorall

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