---

Step * of Lemma fpf-sub-join-left

∀[A:Type]. ∀[B1,B2:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f:a:A fp-> B1[a]]. ∀[g:a:A fp-> Top].  f ⊆ f ⊕ g
BY
{ (Unfolds ``fpf-sub`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B1,B2:A  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f:a:A  fp->  B1[a]].  \mforall{}[g:a:A  fp->  Top].
    f  \msubseteq{}  f  \moplus{}  g


By

---

Latex:
(Unfolds  ``fpf-sub``  0  THEN  Auto)

---

Home Index