---

Step * of Lemma adjacent-to-same2

∀[T:Type]. ∀[L:T List]. ∀[a,b,c:T].
  (b = c ∈ T) supposing (adjacent(T;L;c;a) and adjacent(T;L;b;a) and no_repeats(T;L))
BY
{ ((Auto THEN Using [`z',⌜c⌝] (FLemma `before-adjacent` [6;7])⋅) THEN Auto) }

1
.....antecedent..... 
1. T : Type
2. L : T List
3. a : T
4. b : T
5. c : T
6. no_repeats(T;L)
7. adjacent(T;L;b;a)
8. adjacent(T;L;c;a)
⊢ c before a ∈ L

2
1. T : Type
2. L : T List
3. a : T
4. b : T
5. c : T
6. no_repeats(T;L)
7. adjacent(T;L;b;a)
8. adjacent(T;L;c;a)
9. c before b ∈ L ∨ (c = b ∈ T)
⊢ b = c ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[a,b,c:T].
    (b  =  c)  supposing  (adjacent(T;L;c;a)  and  adjacent(T;L;b;a)  and  no\_repeats(T;L))


By

---

Latex:
((Auto  THEN  Using  [`z',\mkleeneopen{}c\mkleeneclose{}]  (FLemma  `before-adjacent`  [6;7])\mcdot{})  THEN  Auto)

---

Home Index