---

Step * 2 of Lemma l_before_no_repeats


1. T : Type
2. L : T List@i
3. i : ℕ||L||@i
4. j : ℕ||L||@i
5. no_repeats(T;L)
6. L[j] before L[i] ∈ L
7. i < j
⊢ j < i
BY
{ ((Assert ⌜False⌝⋅ THEN Auto)
   THEN (FLemma `l_before_select` [-1] THENA Auto)
   THEN (FLemma `l_before_transitivity` [-3;-1] THENA Auto)
   THEN FLemma `l_before_antisymmetry` [-5;-1]
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List@i
3.  i  :  \mBbbN{}||L||@i
4.  j  :  \mBbbN{}||L||@i
5.  no\_repeats(T;L)
6.  L[j]  before  L[i]  \mmember{}  L
7.  i  <  j
\mvdash{}  j  <  i


By

---

Latex:
((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (FLemma  `l\_before\_select`  [-1]  THENA  Auto)
  THEN  (FLemma  `l\_before\_transitivity`  [-3;-1]  THENA  Auto)
  THEN  FLemma  `l\_before\_antisymmetry`  [-5;-1]
  THEN  Auto)

---

Home Index