---

Step * of Lemma case-term-equal-left'

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, phi ⊢ _}]. ∀[u:{Gamma, phi ⊢ _:A}]. ∀[v:Top]. ∀[x:{Gamma, phi ⊢ _:A}].
  Gamma, phi ⊢ (u ∨ v)=x:A supposing x = u ∈ {Gamma, phi ⊢ _:A}
BY
{ (InstLemma `case-term-equal-left` [] THEN RepeatFor 5 (ParallelLast') THEN Intros THEN ParallelOp -3) }

---

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].
\mforall{}[x:\{Gamma,  phi  \mvdash{}  \_:A\}].
    Gamma,  phi  \mvdash{}  (u  \mvee{}  v)=x:A  supposing  x  =  u


By

---

Latex:
(InstLemma  `case-term-equal-left`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  Intros
  THEN  ParallelOp  -3)

---

Home Index