---

Step * 1 of Lemma llex-irreflexive


1. A : Type
2. < : A ⟶ A ⟶ ℙ
3. ∀a:A. (¬<[a;a])@i
4. L : A List
5. ∃i:ℕ. (i < ||L|| ∧ i < ||L|| ∧ (∀j:ℕi. (L[j] = L[j] ∈ A)) ∧ <[L[i];L[i]])@i
⊢ False
BY
{ (ExRepD THEN InstHyp [⌜L[i]⌝] 3⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  <  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}a:A.  (\mneg{}<[a;a])@i
4.  L  :  A  List
5.  \mexists{}i:\mBbbN{}.  (i  <  ||L||  \mwedge{}  i  <  ||L||  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (L[j]  =  L[j]))  \mwedge{}  <[L[i];L[i]])@i
\mvdash{}  False


By

---

Latex:
(ExRepD  THEN  InstHyp  [\mkleeneopen{}L[i]\mkleeneclose{}]  3\mcdot{}  THEN  Auto)

---

Home Index