---

Step * of Lemma fpf-cap-single1

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[x:A]. ∀[v,z:Top].  (x : v(x)?z ~ v)
BY
{ (((UnivCD THENA Auto) THEN Unfolds ``fpf-cap fpf-single`` 0 THEN Unfold `fpf-dom` 0 THEN Reduce 0 THEN AutoSplit)
   THENA Auto
   ) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[x:A].  \mforall{}[v,z:Top].    (x  :  v(x)?z  \msim{}  v)


By

(((UnivCD  THENA  Auto)
    THEN  Unfolds  ``fpf-cap  fpf-single``  0
    THEN  Unfold  `fpf-dom`  0
    THEN  Reduce  0
    THEN  AutoSplit)
  THENA  Auto
  )

---

Home Index