---

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
{ (UniformUnivCD Auto THEN Try (RemoveUiff) THEN Try (Complete (Auto)) THEN Repeat (MoveToConcl (-1))) }

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:


\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

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

---

Home Index