---

Step * of Lemma case-type-0

No Annotations
∀[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}].
  ∀[A:Top × Top]. ∀[B:{Gamma ⊢ _}].  Gamma ⊢ (if phi then A else B) = B supposing phi = 0(𝔽) ∈ {Gamma ⊢ _:𝔽}
BY
{ ((InstLemma `case-type-same2` [] THEN RepeatFor 2 (ParallelLast'))
   THEN Intros
   THEN (InstLemma `empty-context-subset-lemma6` [⌜Gamma⌝;⌜A⌝;⌜A⌝]⋅ THENA Auto)
   THEN Fold `member` (-1)
   THEN InstHyp [⌜A⌝;⌜1(𝔽)⌝;⌜B⌝] 3⋅) }

1
.....wf..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. ∀[A:{Gamma, phi ⊢ _}]. ∀[psi:{Gamma ⊢ _:𝔽}]. ∀[B:{Gamma, psi ⊢ _}].
     Gamma, psi ⊢ (if phi then A else B) = B supposing Gamma, (phi ∧ psi) ⊢ A = B
4. phi = 0(𝔽) ∈ {Gamma ⊢ _:𝔽}
5. A : Top × Top
6. B : {Gamma ⊢ _}
7. Gamma, 0(𝔽) ⊢ A
⊢ Gamma, phi ⊢ A

2
.....wf..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. ∀[A:{Gamma, phi ⊢ _}]. ∀[psi:{Gamma ⊢ _:𝔽}]. ∀[B:{Gamma, psi ⊢ _}].
     Gamma, psi ⊢ (if phi then A else B) = B supposing Gamma, (phi ∧ psi) ⊢ A = B
4. phi = 0(𝔽) ∈ {Gamma ⊢ _:𝔽}
5. A : Top × Top
6. B : {Gamma ⊢ _}
7. Gamma, 0(𝔽) ⊢ A
⊢ 1(𝔽) ∈ {Gamma ⊢ _:𝔽}

3
.....wf..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. ∀[A:{Gamma, phi ⊢ _}]. ∀[psi:{Gamma ⊢ _:𝔽}]. ∀[B:{Gamma, psi ⊢ _}].
     Gamma, psi ⊢ (if phi then A else B) = B supposing Gamma, (phi ∧ psi) ⊢ A = B
4. phi = 0(𝔽) ∈ {Gamma ⊢ _:𝔽}
5. A : Top × Top
6. B : {Gamma ⊢ _}
7. Gamma, 0(𝔽) ⊢ A
⊢ Gamma, 1(𝔽) ⊢ B

4
.....antecedent..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. ∀[A:{Gamma, phi ⊢ _}]. ∀[psi:{Gamma ⊢ _:𝔽}]. ∀[B:{Gamma, psi ⊢ _}].
     Gamma, psi ⊢ (if phi then A else B) = B supposing Gamma, (phi ∧ psi) ⊢ A = B
4. phi = 0(𝔽) ∈ {Gamma ⊢ _:𝔽}
5. A : Top × Top
6. B : {Gamma ⊢ _}
7. Gamma, 0(𝔽) ⊢ A
⊢ Gamma, (phi ∧ 1(𝔽)) ⊢ A = B

5
1. [Gamma] : CubicalSet{j}
2. [phi] : {Gamma ⊢ _:𝔽}
3. ∀[A:{Gamma, phi ⊢ _}]. ∀[psi:{Gamma ⊢ _:𝔽}]. ∀[B:{Gamma, psi ⊢ _}].
     Gamma, psi ⊢ (if phi then A else B) = B supposing Gamma, (phi ∧ psi) ⊢ A = B
4. [%] : phi = 0(𝔽) ∈ {Gamma ⊢ _:𝔽}
5. [A] : Top × Top
6. [B] : {Gamma ⊢ _}
7. Gamma, 0(𝔽) ⊢ A
8. Gamma, 1(𝔽) ⊢ (if phi then A else B) = B
⊢ Gamma ⊢ (if phi then A else B) = B

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].
    \mforall{}[A:Top  \mtimes{}  Top].  \mforall{}[B:\{Gamma  \mvdash{}  \_\}].    Gamma  \mvdash{}  (if  phi  then  A  else  B)  =  B  supposing  phi  =  0(\mBbbF{})


By

---

Latex:
((InstLemma  `case-type-same2`  []  THEN  RepeatFor  2  (ParallelLast'))
  THEN  Intros
  THEN  (InstLemma  `empty-context-subset-lemma6`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Fold  `member`  (-1)
  THEN  InstHyp  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}1(\mBbbF{})\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]  3\mcdot{})

---

Home Index