---

Step * of Lemma compatible-system_wf

No Annotations
∀[Gamma:j⊢]. ∀[sys:(phi:{Gamma ⊢ _:𝔽} × {Gamma, phi ⊢ _}) List].  (compatible-system{i:l}(Gamma;sys) ∈ ℙ{[i' | j']})
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[sys:(phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}  \mtimes{}  \{Gamma,  phi  \mvdash{}  \_\})  List].
    (compatible-system\{i:l\}(Gamma;sys)  \mmember{}  \mBbbP{}\{[i'  |  j']\})


By

---

Latex:
ProveWfLemma

---

Home Index