---

Step * of Lemma system-type-same

No Annotations
∀[Gamma:j⊢]. ∀[sys:(phi:{Gamma ⊢ _:𝔽} × {Gamma, phi ⊢ _}) List].
  ∀i:ℕ||sys||. Gamma, fst(sys[i]) ⊢ system-type(sys) = snd(sys[i]) supposing compatible-system{i:l}(Gamma;sys)
BY
{ (Intros
   THEN Unfold `same-cubical-type` 0
   THEN (InstLemma `system-type-properties` [⌜Gamma⌝;⌜sys⌝]⋅ THENA Auto)
   THEN D -1
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[sys:(phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}  \mtimes{}  \{Gamma,  phi  \mvdash{}  \_\})  List].
    \mforall{}i:\mBbbN{}||sys||.  Gamma,  fst(sys[i])  \mvdash{}  system-type(sys)  =  snd(sys[i]) 
    supposing  compatible-system\{i:l\}(Gamma;sys)


By

---

Latex:
(Intros
  THEN  Unfold  `same-cubical-type`  0
  THEN  (InstLemma  `system-type-properties`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}sys\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index