---

Step * of Lemma nil-llex

∀[A:Type]. ∀[<:A ⟶ A ⟶ ℙ].  ∀L:A List. ((L = [] ∈ (A List)) ∨ ([] llex(A;a,b.<[a;b]) L))
BY
{ xxx(Auto THEN D -1 THEN Auto THEN OrRight THEN Auto)xxx }

1
1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. u : A
4. v : A List
⊢ [] llex(A;a,b.<[a;b]) [u / v]

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[<:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    \mforall{}L:A  List.  ((L  =  [])  \mvee{}  ([]  llex(A;a,b.<[a;b])  L))


By

---

Latex:
xxx(Auto  THEN  D  -1  THEN  Auto  THEN  OrRight  THEN  Auto)xxx

---

Home Index