---

Step * of Lemma csm-subtype-iso-instance1

No Annotations
∀[X,H:j⊢]. ∀[phi:{H ⊢ _:𝔽}].  (X j⟶ H.𝕀, (phi)p ⊆r X j⟶ H, phi.𝕀)
BY
{ ((Intros THEN (Assert H.𝕀 j⊢ BY Auto) THEN (Assert H, phi.𝕀 j⊢ BY Auto))
   THEN BLemma `csm-subset-codomain`
   THEN Try (BLemma `context-adjoin-subset1`)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,H:j\mvdash{}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].    (X  j{}\mrightarrow{}  H.\mBbbI{},  (phi)p  \msubseteq{}r  X  j{}\mrightarrow{}  H,  phi.\mBbbI{})


By

---

Latex:
((Intros  THEN  (Assert  H.\mBbbI{}  j\mvdash{}  BY  Auto)  THEN  (Assert  H,  phi.\mBbbI{}  j\mvdash{}  BY  Auto))
  THEN  BLemma  `csm-subset-codomain`
  THEN  Try  (BLemma  `context-adjoin-subset1`)
  THEN  Auto)

---

Home Index