---

Step * of Lemma sub-system_weakening

∀[M:Type ─→ Type]. ∀S1,S2:System(P.M[P]).  sub-system(P.M[P];S1;S2) supposing S1 = S2 ∈ System(P.M[P])
BY
{ (Auto
   THEN All (Unfold `System`)
   THEN DVar `S1'
   THEN DVar `S2'
   THEN (EqHD (-1) THENA Auto)
   THEN All Reduce
   THEN RepUR ``sub-system`` 0
   THEN Auto
   THEN (HypSubst (-2) 0 THEN Auto)⋅) }

1
1. [M] : Type ─→ Type
2. S3 : component(P.M[P]) List@i
3. S4 : LabeledDAG(pInTransit(P.M[P]))@i
4. S5 : component(P.M[P]) List@i
5. S6 : LabeledDAG(pInTransit(P.M[P]))@i
6. S3 = S5 ∈ (component(P.M[P]) List)
7. S4 = S6 ∈ LabeledDAG(pInTransit(P.M[P]))
8. S3 ⊆ S5
⊢ S6 ⊆ S6

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}S1,S2:System(P.M[P]).    sub-system(P.M[P];S1;S2)  supposing  S1  =  S2


By

---

Latex:
(Auto
  THEN  All  (Unfold  `System`)
  THEN  DVar  `S1'
  THEN  DVar  `S2'
  THEN  (EqHD  (-1)  THENA  Auto)
  THEN  All  Reduce
  THEN  RepUR  ``sub-system``  0
  THEN  Auto
  THEN  (HypSubst  (-2)  0  THEN  Auto)\mcdot{})

---

Home Index