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

At: decidable equal union
A,B:Type, x,y:A+B. (a1,a2:A. Dec(a1 = a2)) (b1,b2:B. Dec(b1 = b2)) Dec(x = y)
By:
Unfold `decidable` 0
THEN
Analyze 3
THEN
Analyze 4
THEN
AllHyps (h.((InstHyp [x1;x] h) THENA (Complete Auto)) THEN (ParallelOp -1) THEN (ObviousFrom [-1]))
THEN
AllHyps (h.((InstHyp [y1;y2] h) THENA (Complete Auto)) THEN (ParallelOp -1))
Generated subgoals:

11. 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		1 step
 
21. 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		1 step
 
31. 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		1 step
 
41. 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		1 step

About:
decidableunioninlinruniverseequalimpliesorall

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