---

Step * of Lemma fpf-sub-set

∀[A:Type]. ∀[P:A ─→ ℙ]. ∀[B:A ─→ Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:{a:A| P[a]}  fp-> B[a]].  f ⊆ g supposing f ⊆ g
BY
{ (UniformUnivCD Auto THEN Auto) }

1
1. A : Type
2. P : A ─→ ℙ
3. B : A ─→ Type
4. eq : EqDecider(A)
5. f : a:{a:A| P[a]}  fp-> B[a]
6. g : a:{a:A| P[a]}  fp-> B[a]
7. f ⊆ g
⊢ f ⊆ g

---

Latex:


\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f,g:a:\{a:A|  P[a]\}    fp->  B[a]].
    f  \msubseteq{}  g  supposing  f  \msubseteq{}  g


By

(UniformUnivCD  Auto  THEN  Auto)

---

Home Index