---

Step * of Lemma fpf-cap-single

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

---

Latex:


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


By

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

---

Home Index