---

Step * of Lemma case-term-0

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

1
.....assertion..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma ⊢ _}
4. u : Top
5. v : {Gamma ⊢ _:A}
6. phi = 0(𝔽) ∈ {Gamma ⊢ _:𝔽}
⊢ u ∈ {Gamma, phi ⊢ _:A}

2
.....antecedent..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma ⊢ _}
4. u : Top
5. v : {Gamma ⊢ _:A}
6. phi = 0(𝔽) ∈ {Gamma ⊢ _:𝔽}
7. u ∈ {Gamma, phi ⊢ _:A}
⊢ Gamma, (phi ∧ 1(𝔽)) ⊢ u=v:A

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}u  \mmember{}  \{Gamma,  phi  \mvdash{}  \_:A\}\mkleeneclose{}\mcdot{}
            THENM  (InstLemma  `case-term-equal-right`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}1(\mBbbF{})\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
            )
  )

---

Home Index