---

Step * of Lemma case-term-1

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma ⊢ _}]. ∀[u:{Gamma ⊢ _:A}]. ∀[v:Top].
  Gamma ⊢ (u ∨ v)=u:A supposing phi = 1(𝔽) ∈ {Gamma ⊢ _:𝔽}
BY
{ (Auto
   THEN (InstLemma `case-term-equal-left` [⌜Gamma⌝;⌜phi⌝;⌜A⌝;⌜u⌝;⌜v⌝]⋅ THENA Auto)
   THEN ParallelLast
   THEN SubsumeC ⌜{Gamma, phi ⊢ _:A}⌝⋅
   THEN Try (Trivial)) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma ⊢ _}
4. u : {Gamma ⊢ _:A}
5. v : Top
6. phi = 1(𝔽) ∈ {Gamma ⊢ _:𝔽}
7. (u ∨ v) = u ∈ {Gamma, phi ⊢ _:A}
8. (u ∨ v) = u ∈ {Gamma, phi ⊢ _:A}
⊢ {Gamma, phi ⊢ _:A} ⊆r {Gamma ⊢ _:A}

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `case-term-equal-left`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  SubsumeC  \mkleeneopen{}\{Gamma,  phi  \mvdash{}  \_:A\}\mkleeneclose{}\mcdot{}
  THEN  Try  (Trivial))

---

Home Index