---

Step * of Lemma case-type-partition

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}].
  (∀[A:{Gamma, phi ⊢ _}]. ∀[B:{Gamma, psi ⊢ _}].  Gamma ⊢ (if phi then A else B)) supposing 
     (Gamma ⊢ (1(𝔽) ⇒ (phi ∨ psi)) and 
     Gamma ⊢ ((phi ∧ psi) ⇒ 0(𝔽)))
BY
{ ((InstLemma `case-type_wf` [] THEN RepeatFor 3 (ParallelLast'))
   THEN RepeatFor 2 (Intro)
   THEN ParallelOp -3
   THEN ParallelLast'
   THEN (D -1
         THENA ((InstLemma `same-cubical-type-0` [⌜Gamma⌝;⌜A⌝;⌜B⌝]⋅ THENA Auto)
                THEN (ParallelLast THEN SubsumeEqualityType (-1))
                THEN Auto)
         )
   THEN DoSubsume
   THEN Auto
   THEN EAuto 1) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].
    (\mforall{}[A:\{Gamma,  phi  \mvdash{}  \_\}].  \mforall{}[B:\{Gamma,  psi  \mvdash{}  \_\}].    Gamma  \mvdash{}  (if  phi  then  A  else  B))  supposing 
          (Gamma  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  (phi  \mvee{}  psi))  and 
          Gamma  \mvdash{}  ((phi  \mwedge{}  psi)  {}\mRightarrow{}  0(\mBbbF{})))


By

---

Latex:
((InstLemma  `case-type\_wf`  []  THEN  RepeatFor  3  (ParallelLast'))
  THEN  RepeatFor  2  (Intro)
  THEN  ParallelOp  -3
  THEN  ParallelLast'
  THEN  (D  -1
              THENA  ((InstLemma  `same-cubical-type-0`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (ParallelLast  THEN  SubsumeEqualityType  (-1))
                            THEN  Auto)
              )
  THEN  DoSubsume
  THEN  Auto
  THEN  EAuto  1)

---

Home Index