---

Step * of Lemma case-term-1'

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma ⊢ _}]. ∀[u,x:{Gamma ⊢ _:A}]. ∀[v:Top].
  (Gamma ⊢ (u ∨ v)=x:A) supposing ((x = u ∈ {Gamma ⊢ _:A}) and (phi = 1(𝔽) ∈ {Gamma ⊢ _:𝔽}))
BY
{ (InstLemma `case-term-1` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Intros
   THEN (Assert Gamma ⊢ (u ∨ v)=u:A BY
               (BackThruSomeHyp THEN Auto))
   THEN ParallelLast) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `case-term-1`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Intros
  THEN  (Assert  Gamma  \mvdash{}  (u  \mvee{}  v)=u:A  BY
                          (BackThruSomeHyp  THEN  Auto))
  THEN  ParallelLast)

---

Home Index