---

Step * of Lemma decode-equivTerm

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}].  (decode(equivTerm(G;A;B)) = Equiv(decode(A);decode(B)) ∈ {G ⊢ _})
BY
{ (Intros⋅ THEN Unfold `equivTerm` 0 THEN BLemma `universe-decode-encode` THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].    (decode(equivTerm(G;A;B))  =  Equiv(decode(A);decode(B)))


By

---

Latex:
(Intros\mcdot{}  THEN  Unfold  `equivTerm`  0  THEN  BLemma  `universe-decode-encode`  THEN  Auto)

---

Home Index