---

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

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, (phi ∨ psi) ⊢ _}]. ∀[u:{Gamma, phi ⊢ _:A}].
∀[v,x:{Gamma, psi ⊢ _:A}].
  (Gamma, psi ⊢ (u ∨ v)=x:A) supposing ((x = v ∈ {Gamma, psi ⊢ _:A}) and Gamma, (phi ∧ psi) ⊢ u=v:A)
BY
{ (InstLemma `case-term-equal-right` []
   THEN RepeatFor 6 (ParallelLast')
   THEN Intros
   THEN ThinTrivial
   THEN ParallelLast) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `case-term-equal-right`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  Intros
  THEN  ThinTrivial
  THEN  ParallelLast)

---

Home Index