---

Step * 1 of Lemma poset-functor_wf


1. J : Cname List
2. K : Cname List
3. f : name-morph(J;K)
4. g : name-morph(K;[])
5. h : name-morph(K;[])
6. p : ∀x@0:nameset(K). (↑g x@0 ≤z h x@0)
7. x : nameset(J)
⊢ ((f o g) x) ≤ ((f o h) x)
BY
{ (RepUR ``name-comp uext`` 0
   THEN (BoolCase ⌜isname(f x)⌝⋅ THENA Auto)
   THEN (FLemma `assert-isname` [-1] ORELSE FLemma `not-assert-isname` [-1])
   THEN Auto
   THEN ((RW assert_pushupC 0 THENM BackThruSomeHyp) THENA Auto)) }

---

Latex:

---

Latex:

1.  J  :  Cname  List
2.  K  :  Cname  List
3.  f  :  name-morph(J;K)
4.  g  :  name-morph(K;[])
5.  h  :  name-morph(K;[])
6.  p  :  \mforall{}x@0:nameset(K).  (\muparrow{}g  x@0  \mleq{}z  h  x@0)
7.  x  :  nameset(J)
\mvdash{}  ((f  o  g)  x)  \mleq{}  ((f  o  h)  x)


By

---

Latex:
(RepUR  ``name-comp  uext``  0
  THEN  (BoolCase  \mkleeneopen{}isname(f  x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (FLemma  `assert-isname`  [-1]  ORELSE  FLemma  `not-assert-isname`  [-1])
  THEN  Auto
  THEN  ((RW  assert\_pushupC  0  THENM  BackThruSomeHyp)  THENA  Auto))

---

Home Index