---

Step * of Lemma poset-cat-arrow-equals

No Annotations
∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))]. ∀[a:cat-arrow(poset-cat(I)) x y].
  (a = (λx.Ax) ∈ (cat-arrow(poset-cat(I)) x y))
BY
{ (Auto THEN BLemma `poset-cat-arrow-unique` THEN Auto) }

1
.....wf..... 
1. I : Cname List
2. x : cat-ob(poset-cat(I))
3. y : cat-ob(poset-cat(I))
4. a : cat-arrow(poset-cat(I)) x y
⊢ λx.Ax ∈ cat-arrow(poset-cat(I)) x y

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:Cname  List].  \mforall{}[x,y:cat-ob(poset-cat(I))].  \mforall{}[a:cat-arrow(poset-cat(I))  x  y].    (a  =  (\mlambda{}x.Ax))


By

---

Latex:
(Auto  THEN  BLemma  `poset-cat-arrow-unique`  THEN  Auto)

---

Home Index