---

Step * of Lemma fpf-union-contains

∀[A:Type]. ∀[B:A ─→ Type].
  ∀eq:EqDecider(A). ∀f,g:x:A fp-> B[x] List. ∀x:A. ∀R:∩a:A. ((B[a] List) ─→ B[a] ─→ 𝔹).  f(x)?[] ⊆ fpf-union(f;g;eq;R;x)
BY
{ (RepUR ``fpf-union fpf-cap`` 0
   THEN Auto
   THEN (AutoBoolCase ⌈x ∈ dom(f)⌉⋅ THEN Auto)
   THEN (IsectHD ⌈x⌉ 7⋅ THENA Auto)
   THEN AutoBoolCase ⌈x ∈ dom(g)⌉⋅
   THEN Auto) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}eq:EqDecider(A).  \mforall{}f,g:x:A  fp->  B[x]  List.  \mforall{}x:A.  \mforall{}R:\mcap{}a:A.  ((B[a]  List)  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbB{}).
        f(x)?[]  \msubseteq{}  fpf-union(f;g;eq;R;x)


By

(RepUR  ``fpf-union  fpf-cap``  0
  THEN  Auto
  THEN  (AutoBoolCase  \mkleeneopen{}x  \mmember{}  dom(f)\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (IsectHD  \mkleeneopen{}x\mkleeneclose{}  7\mcdot{}  THENA  Auto)
  THEN  AutoBoolCase  \mkleeneopen{}x  \mmember{}  dom(g)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index