---

Step * of Lemma fpf-cap-single1

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

---

Latex:

---

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


By

---

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

---

Home Index