Step
*
of Lemma
adjacent-to-same
∀[T:Type]. ∀[L:T List]. ∀[a,b,c:T].
  (b = c ∈ T) supposing (adjacent(T;L;a;c) and adjacent(T;L;a;b) and no_repeats(T;L))
BY
{ ((Auto THEN Using [`z',⌜c⌝] (FLemma `before-adjacent2` [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;a;b)
8. adjacent(T;L;a;c)
⊢ a before c ∈ 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;a;b)
8. adjacent(T;L;a;c)
9. b before c ∈ 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;a;c)  and  adjacent(T;L;a;b)  and  no\_repeats(T;L))
By
Latex:
((Auto  THEN  Using  [`z',\mkleeneopen{}c\mkleeneclose{}]  (FLemma  `before-adjacent2`  [6;7])\mcdot{})  THEN  Auto)
Home
Index