---

Step * of Lemma fpf-join-sub2

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[eq:EqDecider(A)]. ∀[f1,g,f2:a:A fp-> B[a]].  (f1 ⊕ f2 ⊆ g) supposing (f2 ⊆ g and f1 ⊆ g)
BY
{ xxx(UniformUnivCD Auto THEN Try (RemoveUiff) THEN Try (Complete (Auto)) THEN Repeat (MoveToConcl (-1)))xxx }

1
∀A:Type. ∀B:A ⟶ Type. ∀eq:EqDecider(A). ∀f1,g,f2:a:A fp-> B[a].  (f1 ⊆ g ⇒ f2 ⊆ g ⇒ f1 ⊕ f2 ⊆ g)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f1,g,f2:a:A  fp->  B[a]].
    (f1  \moplus{}  f2  \msubseteq{}  g)  supposing  (f2  \msubseteq{}  g  and  f1  \msubseteq{}  g)


By

---

Latex:
xxx(UniformUnivCD  Auto
        THEN  Try  (RemoveUiff)
        THEN  Try  (Complete  (Auto))
        THEN  Repeat  (MoveToConcl  (-1)))xxx

---

Home Index