---

Step * of Lemma fiber-comp-subset

∀[X,T,A,w,a,cT,cA,phi:Top].  (fiber-comp(X, phi;T;A;w;a;cT;cA) ~ fiber-comp(X;T;A;w;a;cT;cA))
BY
{ (Intros
   THEN RepUR ``fiber-comp case-type-comp sigma_comp`` 0
   THEN RepeatFor 7 (EqCD)
   THEN Try (Trivial)
   THEN (Progress(Unfold `path_comp` 0) ORELSE CsmUnfoldingComp)
   THEN RepUR ``csm-comp-structure`` 0
   THEN RepeatFor 7 (EqCD)
   THEN Try (Trivial)
   THEN CsmUnfolding
   THEN Try (Trivial)) }

---

Latex:

---

Latex:
\mforall{}[X,T,A,w,a,cT,cA,phi:Top].    (fiber-comp(X,  phi;T;A;w;a;cT;cA)  \msim{}  fiber-comp(X;T;A;w;a;cT;cA))


By

---

Latex:
(Intros
  THEN  RepUR  ``fiber-comp  case-type-comp  sigma\_comp``  0
  THEN  RepeatFor  7  (EqCD)
  THEN  Try  (Trivial)
  THEN  (Progress(Unfold  `path\_comp`  0)  ORELSE  CsmUnfoldingComp)
  THEN  RepUR  ``csm-comp-structure``  0
  THEN  RepeatFor  7  (EqCD)
  THEN  Try  (Trivial)
  THEN  CsmUnfolding
  THEN  Try  (Trivial))

---

Home Index