---

Step * of Lemma subtype_rel_record+

∀[T1,T2:𝕌']. ∀[B1:T1 ⟶ 𝕌']. ∀[B2:T2 ⟶ 𝕌'].
  (∀[z:Atom]. (T1z:B1[self] ⊆r T2z:B2[self])) supposing ((∀x:T1. (B1[x] ⊆r B2[x])) and (T1 ⊆r T2))
BY
{ xxx((UnivCD THENA Auto)
      THEN Unfold `record+` 0
      THEN RepeatFor 2 ((SubtypeReasoning1 THEN Try (Complete (Auto))))
      THEN xxxBLemmaUp `subtype_rel_dep_function`xxx
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T1,T2:\mBbbU{}'].  \mforall{}[B1:T1  {}\mrightarrow{}  \mBbbU{}'].  \mforall{}[B2:T2  {}\mrightarrow{}  \mBbbU{}'].
    (\mforall{}[z:Atom].  (T1z:B1[self]  \msubseteq{}r  T2z:B2[self]))  supposing  ((\mforall{}x:T1.  (B1[x]  \msubseteq{}r  B2[x]))  and  (T1  \msubseteq{}r  T2))


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  Unfold  `record+`  0
        THEN  RepeatFor  2  ((SubtypeReasoning1  THEN  Try  (Complete  (Auto))))
        THEN  xxxBLemmaUp  `subtype\_rel\_dep\_function`xxx
        THEN  Auto)xxx

---

Home Index