---

Step * of Lemma subtype-fpf2

∀[A:Type]. ∀[B1,B2:A ─→ Type].  a:A fp-> B1[a] ⊆r a:A fp-> B2[a] supposing ∀a:A. (B1[a] ⊆r B2[a])
BY
{ (Unfold `fpf` 0 THEN Auto) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[B1,B2:A  {}\mrightarrow{}  Type].    a:A  fp->  B1[a]  \msubseteq{}r  a:A  fp->  B2[a]  supposing  \mforall{}a:A.  (B1[a]  \msubseteq{}r  B2[a])


By

(Unfold  `fpf`  0  THEN  Auto)

---

Home Index