---

Step * of Lemma same-cubical-type-by-list-cases

No Annotations
∀[Gamma:j⊢]. ∀L:{Gamma ⊢ _:𝔽} List. ∀A,B:{Gamma, \/(L) ⊢ _}.  Gamma, \/(L) ⊢ A = B supposing (∀phi∈L.Gamma, phi ⊢ A = B)
BY
{ (RepeatFor 2 (Intro)
   THEN InstLemma `list_induction` [⌜parm{[i' | j']}⌝;⌜{Gamma ⊢ _:𝔽}⌝;⌜λ2L.∀A,B:{Gamma, \/(L) ⊢ _}.
                                                                             Gamma, \/(L) ⊢ A = B 
                                                                             supposing (∀phi∈L.Gamma, phi ⊢ A = B)⌝]⋅
   ) }

1
.....wf..... 
1. Gamma : CubicalSet{j}
2. L : {Gamma ⊢ _:𝔽} List
⊢ {Gamma ⊢ _:𝔽} ∈ 𝕌{[i' | j']}

2
.....wf..... 
1. Gamma : CubicalSet{j}
2. L : {Gamma ⊢ _:𝔽} List
⊢ λL.∀A,B:{Gamma, \/(L) ⊢ _}.  Gamma, \/(L) ⊢ A = B supposing (∀phi∈L.Gamma, phi ⊢ A = B) ∈ ({Gamma ⊢ _:𝔽} List)
  ⟶ ℙ{[i' | j']}

3
.....antecedent..... 
1. [Gamma] : CubicalSet{j}
2. L : {Gamma ⊢ _:𝔽} List
⊢ ∀A,B:{Gamma, \/([]) ⊢ _}.  Gamma, \/([]) ⊢ A = B supposing (∀phi∈[].Gamma, phi ⊢ A = B)

4
.....antecedent..... 
1. [Gamma] : CubicalSet{j}
2. L : {Gamma ⊢ _:𝔽} List
⊢ ∀aaaa:{Gamma ⊢ _:𝔽}. ∀LLLL:{Gamma ⊢ _:𝔽} List.
    ((∀A,B:{Gamma, \/(LLLL) ⊢ _}.  Gamma, \/(LLLL) ⊢ A = B supposing (∀phi∈LLLL.Gamma, phi ⊢ A = B))
    ⇒ (∀A,B:{Gamma, \/([aaaa / LLLL]) ⊢ _}.
          Gamma, \/([aaaa / LLLL]) ⊢ A = B supposing (∀phi∈[aaaa / LLLL].Gamma, phi ⊢ A = B)))

5
1. [Gamma] : CubicalSet{j}
2. L : {Gamma ⊢ _:𝔽} List
3. ∀L:{Gamma ⊢ _:𝔽} List. ∀A,B:{Gamma, \/(L) ⊢ _}.  Gamma, \/(L) ⊢ A = B supposing (∀phi∈L.Gamma, phi ⊢ A = B)
⊢ ∀A,B:{Gamma, \/(L) ⊢ _}.  Gamma, \/(L) ⊢ A = B supposing (∀phi∈L.Gamma, phi ⊢ A = B)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}]
    \mforall{}L:\{Gamma  \mvdash{}  \_:\mBbbF{}\}  List.  \mforall{}A,B:\{Gamma,  \mbackslash{}/(L)  \mvdash{}  \_\}.
        Gamma,  \mbackslash{}/(L)  \mvdash{}  A  =  B  supposing  (\mforall{}phi\mmember{}L.Gamma,  phi  \mvdash{}  A  =  B)


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  InstLemma  `list\_induction`  [\mkleeneopen{}parm\{[i'  |  j']\}\mkleeneclose{};\mkleeneopen{}\{Gamma  \mvdash{}  \_:\mBbbF{}\}\mkleeneclose{};
            \mkleeneopen{}\mlambda{}\msubtwo{}L.\mforall{}A,B:\{Gamma,  \mbackslash{}/(L)  \mvdash{}  \_\}.    Gamma,  \mbackslash{}/(L)  \mvdash{}  A  =  B  supposing  (\mforall{}phi\mmember{}L.Gamma,  phi  \mvdash{}  A  =  B)\mkleeneclose{}]\mcdot{}
  )

---

Home Index