---

Step * of Lemma discrete-pathtype-uniform

No Annotations
∀[T:Type]. ∀[X,Z:j⊢]. ∀[s:Z j⟶ X]. ∀[pth:{Z ⊢ _:(Path(discr(T)))s}].
  (pth = refl(pth @ 0(𝕀)) ∈ {Z ⊢ _:(Path(discr(T)))s})
BY
{ ((Auto THEN UsingVars [`T'] (BLemma `discrete-pathtype`)) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[X,Z:j\mvdash{}].  \mforall{}[s:Z  j{}\mrightarrow{}  X].  \mforall{}[pth:\{Z  \mvdash{}  \_:(Path(discr(T)))s\}].    (pth  =  refl(pth  @  0(\mBbbI{})))


By

---

Latex:
((Auto  THEN  UsingVars  [`T']  (BLemma  `discrete-pathtype`))  THEN  Auto)

---

Home Index