---

Step * of Lemma ma-state-subtype2

∀[ds,ds':ltg:Id fp-> Type].  State(ds') ⊆ State(ds) supposing ds ⊆ ds'
BY
{ (Auto THEN D 0 THEN Auto THEN DoSubsume THEN Auto THEN BLemma `ma-state-subtype` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[ds,ds':ltg:Id  fp->  Type].    State(ds')  \msubseteq{}  State(ds)  supposing  ds  \msubseteq{}  ds'


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  DoSubsume  THEN  Auto  THEN  BLemma  `ma-state-subtype`  THEN  Auto)

---

Home Index