---

Step * of Lemma fpf-join-ap-sq

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> Top]. ∀[g:Top]. ∀[x:A].  (f ⊕ g(x) ~ if x ∈ dom(f) then f(x) else g(x) fi )
BY
{ ((UnivCD THENA Auto)
   THEN Repeat ((Unfolds ``fpf-join fpf-ap fpf-cap`` 0 THEN Reduce 0))
   THEN SplitOnConclITE
   THEN Auto) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f:a:A  fp->  Top].  \mforall{}[g:Top].  \mforall{}[x:A].
    (f  \moplus{}  g(x)  \msim{}  if  x  \mmember{}  dom(f)  then  f(x)  else  g(x)  fi  )


By

((UnivCD  THENA  Auto)
  THEN  Repeat  ((Unfolds  ``fpf-join  fpf-ap  fpf-cap``  0  THEN  Reduce  0))
  THEN  SplitOnConclITE
  THEN  Auto)

---

Home Index