---

Step * of Lemma subtype-fpf-cap

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type].  {∀[x:X]. (f(x)?Top ⊆r g(x)?Top)} supposing g ⊆ f
BY
{ (((Unfold `guard` 0
     THEN Auto
     THEN D 0
     THEN Auto
     THEN (All (Unfold `fpf-cap`))
     THEN (MoveToConcl (-1))
     THEN SplitOnConclITE)
    THENA Auto
    )
   THEN SplitOnConclITE
   THEN Auto
   THEN (Unfold `fpf-sub` (-5))
   THEN (InstHyp [⌈x⌉] (-5))⋅
   THEN ExRepD
   THEN Auto) }

---

Latex:


\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].  \mforall{}[f,g:x:X  fp->  Type].
    \{\mforall{}[x:X].  (f(x)?Top  \msubseteq{}r  g(x)?Top)\}  supposing  g  \msubseteq{}  f


By

(((Unfold  `guard`  0
      THEN  Auto
      THEN  D  0
      THEN  Auto
      THEN  (All  (Unfold  `fpf-cap`))
      THEN  (MoveToConcl  (-1))
      THEN  SplitOnConclITE)
    THENA  Auto
    )
  THEN  SplitOnConclITE
  THEN  Auto
  THEN  (Unfold  `fpf-sub`  (-5))
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-5))\mcdot{}
  THEN  ExRepD
  THEN  Auto)

---

Home Index