---

Step * 1 of Lemma strong-subtype-set3


1. A : Type
2. B : Type
3. P : A ⟶ ℙ
4. strong-subtype(A;B)
5. strong-subtype({x:A| P[x]} ;{x:B| λx.True[x]} )
6. strong-subtype({x:B| λx.True[x]} ;B)
⊢ strong-subtype({x:A| P x} ;B)
BY
{ ((Using [`B',⌜{x:B| λx.True[x]} ⌝] (BLemma `strong-subtype_transitivity`))⋅ THEN Auto THEN ReduceSOAps 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  P  :  A  {}\mrightarrow{}  \mBbbP{}
4.  strong-subtype(A;B)
5.  strong-subtype(\{x:A|  P[x]\}  ;\{x:B|  \mlambda{}x.True[x]\}  )
6.  strong-subtype(\{x:B|  \mlambda{}x.True[x]\}  ;B)
\mvdash{}  strong-subtype(\{x:A|  P  x\}  ;B)


By

---

Latex:
((Using  [`B',\mkleeneopen{}\{x:B|  \mlambda{}x.True[x]\}  \mkleeneclose{}]  (BLemma  `strong-subtype\_transitivity`))\mcdot{}
  THEN  Auto
  THEN  ReduceSOAps  0
  THEN  Auto)

---

Home Index