---

Step * of Lemma case-term-0'

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

---

Latex:

---

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


By

---

Latex:
(InstLemma  `case-term-0`  []  THEN  RepeatFor  5  (ParallelLast')  THEN  Auto  THEN  ParallelLast)

---

Home Index