---

Step * of Lemma subtype_rel_dep_function

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[C:Type]. ∀[D:C ⟶ Type].
  ((a:A ⟶ B[a]) ⊆r (c:C ⟶ D[c])) supposing ((∀a:C. (B[a] ⊆r D[a])) and (C ⊆r A))
BY
{ (Auto THEN D 0 THEN Auto THEN FunExt THEN Auto THEN All (Unfold `so_apply`) THEN DoSubsume THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[C:Type].  \mforall{}[D:C  {}\mrightarrow{}  Type].
    ((a:A  {}\mrightarrow{}  B[a])  \msubseteq{}r  (c:C  {}\mrightarrow{}  D[c]))  supposing  ((\mforall{}a:C.  (B[a]  \msubseteq{}r  D[a]))  and  (C  \msubseteq{}r  A))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  FunExt
  THEN  Auto
  THEN  All  (Unfold  `so\_apply`)
  THEN  DoSubsume
  THEN  Auto)

---

Home Index