---

Step * of Lemma case-term-equal-left

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, phi ⊢ _}]. ∀[u:{Gamma, phi ⊢ _:A}]. ∀[v:Top].  Gamma, phi ⊢ (u ∨ v)=u:A
BY
{ (Auto
   THEN UnfoldTopAb 0
   THEN Symmetry
   THEN (Assert ⌜u = (u ∨ v) ∈ (I:fset(ℕ) ⟶ a:Gamma, phi(I) ⟶ A(a))⌝⋅
   THENM (BLemma `cubical-term-equal` THEN Auto)
   )) }

1
.....assertion..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma, phi ⊢ _}
4. u : {Gamma, phi ⊢ _:A}
5. v : Top
⊢ u = (u ∨ v) ∈ (I:fset(ℕ) ⟶ a:Gamma, phi(I) ⟶ A(a))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma,  phi  \mvdash{}  \_\}].  \mforall{}[u:\{Gamma,  phi  \mvdash{}  \_:A\}].  \mforall{}[v:Top].
    Gamma,  phi  \mvdash{}  (u  \mvee{}  v)=u:A


By

---

Latex:
(Auto
  THEN  UnfoldTopAb  0
  THEN  Symmetry
  THEN  (Assert  \mkleeneopen{}u  =  (u  \mvee{}  v)\mkleeneclose{}\mcdot{}  THENM  (BLemma  `cubical-term-equal`  THEN  Auto)))

---

Home Index