---

Step * of Lemma before-map

∀[T,T':Type].
  ∀f:T ⟶ T'. ∀L:T List. ∀x',y':T'.
    (x' before y' ∈ map(f;L) ⇐⇒ ∃x,y:T. (x before y ∈ L ∧ ((f x) = x' ∈ T') ∧ ((f y) = y' ∈ T')))
BY
{ (InductionOnList THEN Reduce 0) }

1
1. [T] : Type
2. [T'] : Type
3. f : T ⟶ T'
⊢ ∀x',y':T'.  (x' before y' ∈ [] ⇐⇒ ∃x,y:T. (x before y ∈ [] ∧ ((f x) = x' ∈ T') ∧ ((f y) = y' ∈ T')))

2
1. [T] : Type
2. [T'] : Type
3. f : T ⟶ T'
4. u : T
5. v : T List
6. ∀x',y':T'.  (x' before y' ∈ map(f;v) ⇐⇒ ∃x,y:T. (x before y ∈ v ∧ ((f x) = x' ∈ T') ∧ ((f y) = y' ∈ T')))
⊢ ∀x',y':T'.
    (x' before y' ∈ [f u / map(f;v)] ⇐⇒ ∃x,y:T. (x before y ∈ [u / v] ∧ ((f x) = x' ∈ T') ∧ ((f y) = y' ∈ T')))

---

Latex:

---

Latex:
\mforall{}[T,T':Type].
    \mforall{}f:T  {}\mrightarrow{}  T'.  \mforall{}L:T  List.  \mforall{}x',y':T'.
        (x'  before  y'  \mmember{}  map(f;L)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x,y:T.  (x  before  y  \mmember{}  L  \mwedge{}  ((f  x)  =  x')  \mwedge{}  ((f  y)  =  y')))


By

---

Latex:
(InductionOnList  THEN  Reduce  0)

---

Home Index