---

Step * of Lemma fpf-join-domain

∀[A:Type]. ∀f,g:a:A fp-> Top. ∀eq:EqDecider(A).  fpf-domain(f ⊕ g) ⊆ fpf-domain(f) @ fpf-domain(g)
BY
{ (Auto
   THEN Unfold `l_contains` 0
   THEN (BLemma `l_all_iff` THENA Auto)
   THEN RWO "fpf-domain-join" 0
   THEN Auto
   THEN RWO "member_append" 0
   THEN Auto) }

---

Latex:


\mforall{}[A:Type].  \mforall{}f,g:a:A  fp->  Top.  \mforall{}eq:EqDecider(A).    fpf-domain(f  \moplus{}  g)  \msubseteq{}  fpf-domain(f)  @  fpf-domain(g)


By

(Auto
  THEN  Unfold  `l\_contains`  0
  THEN  (BLemma  `l\_all\_iff`  THENA  Auto)
  THEN  RWO  "fpf-domain-join"  0
  THEN  Auto
  THEN  RWO  "member\_append"  0
  THEN  Auto)

---

Home Index