---

Step * of Lemma subtype_rel_record+_easy

∀[T1,T2:𝕌']. ∀[B:T2 ⟶ 𝕌'].  ∀[z:Atom]. (T1; z:B[self] ⊆r T2; z:B[self]) supposing T1 ⊆r T2
BY
{ (InstLemma `subtype_rel_record+` [] THEN RepeatFor 2 (ParallelLast') THEN Auto THEN BHyp 3  THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T1,T2:\mBbbU{}'].  \mforall{}[B:T2  {}\mrightarrow{}  \mBbbU{}'].    \mforall{}[z:Atom].  (T1;  z:B[self]  \msubseteq{}r  T2;  z:B[self])  supposing  T1  \msubseteq{}r  T2


By

---

Latex:
(InstLemma  `subtype\_rel\_record+`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  BHyp  3 
  THEN  Auto)

---

Home Index