---

Step * 1 of Lemma nil-llex


1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. u : A
4. v : A List
⊢ [] llex(A;a,b.<[a;b]) [u / v]
BY
{ (RepUR ``llex`` 0 THEN OrLeft THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [<]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  u  :  A
4.  v  :  A  List
\mvdash{}  []  llex(A;a,b.<[a;b])  [u  /  v]


By

---

Latex:
(RepUR  ``llex``  0  THEN  OrLeft  THEN  Auto)

---

Home Index