---

Step * of Lemma constrained-cubical-term-eqcd

No Annotations
∀[Gamma:j⊢]. ∀[A,B:{Gamma ⊢ _}]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[t:{Gamma, phi ⊢ _:A}]. ∀[t':{Gamma, psi ⊢ _:B}].
  ({Gamma ⊢ _:A[phi |⟶ t]} = {Gamma ⊢ _:B[psi |⟶ t']} ∈ 𝕌{[i | j']}) supposing 
     ((t' = t ∈ {Gamma, phi ⊢ _:A}) and 
     (phi = psi ∈ {Gamma ⊢ _:𝔽}) and 
     (A = B ∈ {Gamma ⊢ _}))
BY
{ (RepeatFor 9 (Intro)
   THEN (Assert {Gamma, phi ⊢ _:A} = {Gamma, psi ⊢ _:B} ∈ 𝕌{[i | j']} BY
               (EqCDA THEN Auto THEN CTTLevelToI THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A,B:\{Gamma  \mvdash{}  \_\}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[t:\{Gamma,  phi  \mvdash{}  \_:A\}].
\mforall{}[t':\{Gamma,  psi  \mvdash{}  \_:B\}].
    (\{Gamma  \mvdash{}  \_:A[phi  |{}\mrightarrow{}  t]\}  =  \{Gamma  \mvdash{}  \_:B[psi  |{}\mrightarrow{}  t']\})  supposing 
          ((t'  =  t)  and 
          (phi  =  psi)  and 
          (A  =  B))


By

---

Latex:
(RepeatFor  9  (Intro)
  THEN  (Assert  \{Gamma,  phi  \mvdash{}  \_:A\}  =  \{Gamma,  psi  \mvdash{}  \_:B\}  BY
                          (EqCDA  THEN  Auto  THEN  CTTLevelToI  THEN  Auto))
  THEN  Auto)

---

Home Index