---

Step * of Lemma decidable__equal-poset-cat-ob

∀I:Cname List. ∀c1,c2:cat-ob(poset-cat(I)).  Dec(c1 = c2 ∈ cat-ob(poset-cat(I)))
BY
{ (InstLemma `poset-cat-ob-cases` [] THEN RepeatFor 3 (ParallelLast') THEN Unfold `decidable` 0 THEN ParallelLast) }

1
1. I : Cname List@i
2. c1 : cat-ob(poset-cat(I))@i
3. c2 : cat-ob(poset-cat(I))@i
4. ∃y:nameset(I). c1 y ≠ c2 y
⊢ ¬(c1 = c2 ∈ cat-ob(poset-cat(I)))

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}c1,c2:cat-ob(poset-cat(I)).    Dec(c1  =  c2)


By

---

Latex:
(InstLemma  `poset-cat-ob-cases`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Unfold  `decidable`  0
  THEN  ParallelLast)

---

Home Index