---

Step * of Lemma fpf-cap-single-join

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[x:A]. ∀[v,z,f:Top].  (x : v ⊕ f(x)?z ~ v)
BY
{ ((((UnivCD THENA Auto) THEN RepUR ``fpf-join fpf-cap fpf-single fpf-ap fpf-dom`` 0 THEN AutoSplit) THENA Auto)
   THEN Reduce 0
   THEN Try (Trivial)) }

---

Latex:


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


By

((((UnivCD  THENA  Auto)  THEN  RepUR  ``fpf-join  fpf-cap  fpf-single  fpf-ap  fpf-dom``  0  THEN  AutoSplit)
    THENA  Auto
    )
  THEN  Reduce  0
  THEN  Try  (Trivial))

---

Home Index