---

Step * of Lemma subtype-fpf-cap-void-list

∀[X:Type]. ∀[eq:EqDecider(X)]. ∀[f,g:x:X fp-> Type]. ∀[x:X].  (f(x)?Void List) ⊆r (g(x)?Void List) supposing f ⊆ g
BY
{ xxx((((Auto THEN D 0) THENA Auto) THEN (All (Unfolds ``fpf-sub fpf-cap``)) THEN (SplitOnHypITE (-1))) THENA Auto)xxx }

---

Latex:

---

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


By

---

Latex:
xxx((((Auto  THEN  D  0)  THENA  Auto)
          THEN  (All  (Unfolds  ``fpf-sub  fpf-cap``))
          THEN  (SplitOnHypITE  (-1)))
        THENA  Auto
        )xxx

---

Home Index