---

Step * of Lemma csm-subtype-iso-instance2

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

---

Latex:

---

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


By

---

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

---

Home Index