---

Step * of Lemma fpf-union_wf

∀[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] ─→ 𝔹)].
  (fpf-union(f;g;eq;R;x) ∈ B[x] List)
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{})].
    (fpf-union(f;g;eq;R;x)  \mmember{}  B[x]  List)


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