Step * of Lemma fpf-join-dom

`∀[A:Type]. ∀[B:A ─→ Type].`
`  ∀eq:EqDecider(A). ∀f,g:a:A fp-> B[a]. ∀x:A.  (↑x ∈ dom(f ⊕ g) `⇐⇒` (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g)))`
BY
`{ (((((((((Unfolds ``fpf fpf-join fpf-dom`` 0 THEN Unfold `fpf-dom` 0 THEN Reduce 0 THEN UnivCD) THENA Auto)`
`         THEN RWO "assert-deq-member" 0`
`         )`
`        THENA Auto`
`        )`
`       THEN RWO "member_append" 0`
`       )`
`      THENA Auto`
`      )`
`     THEN RWO "member_filter" 0`
`     )`
`    THENA (Reduce 0 THEN Auto)`
`    )`
`   THEN Reduce 0`
`   THEN AutoBoolCase ⌈x ∈b fst(f))⌉⋅) }`

Latex:

\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
\mforall{}eq:EqDecider(A).  \mforall{}f,g:a:A  fp->  B[a].  \mforall{}x:A.    (\muparrow{}x  \mmember{}  dom(f  \moplus{}  g)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}x  \mmember{}  dom(f))  \mvee{}  (\muparrow{}x  \mmember{}  dom(g)))

By

(((((((((Unfolds  ``fpf  fpf-join  fpf-dom``  0  THEN  Unfold  `fpf-dom`  0  THEN  Reduce  0  THEN  UnivCD)
THENA  Auto
)
THEN  RWO  "assert-deq-member"  0
)
THENA  Auto
)
THEN  RWO  "member\_append"  0
)
THENA  Auto
)
THEN  RWO  "member\_filter"  0
)
THENA  (Reduce  0  THEN  Auto)
)
THEN  Reduce  0
THEN  AutoBoolCase  \mkleeneopen{}x  \mmember{}\msubb{}  fst(f))\mkleeneclose{}\mcdot{})

Home Index