---

Step * of Lemma term-to-pathtype-beta

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}].  ∀r:{G ⊢ _:𝕀}. ∀a:{G.𝕀 ⊢ _:(A)p}.  (<>a @ r = (a)[r] ∈ {G ⊢ _:A})
BY
{ (InstLemma `term-to-path-beta` [] THEN Unfold `term-to-pathtype` 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].    \mforall{}r:\{G  \mvdash{}  \_:\mBbbI{}\}.  \mforall{}a:\{G.\mBbbI{}  \mvdash{}  \_:(A)p\}.    (<>a  @  r  =  (a)[r])


By

---

Latex:
(InstLemma  `term-to-path-beta`  []  THEN  Unfold  `term-to-pathtype`  0  THEN  Auto)

---

Home Index