---

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
{ xxx(((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)xxx }

---

Latex:

---

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

---

Latex:
xxx(((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)xxx

---

Home Index