---

Step * 1 of Lemma map_functionality_wrt_sq


1. T : Type
2. T ⊆r Base
3. f : Base
4. g : Base
5. L : T List
⊢ map(f;L) ~ map(g;L) supposing ∀x:T. ((x ∈ L) ⇒ (f x ~ g x))
BY
{ (ListInd (-1) THEN Reduce 0) }

1
1. T : Type
2. T ⊆r Base
3. f : Base
4. g : Base
⊢ [] ~ [] supposing ∀x:T. ((x ∈ []) ⇒ (f x ~ g x))

2
1. T : Type
2. T ⊆r Base
3. f : Base
4. g : Base
5. u : T
6. v : T List
7. map(f;v) ~ map(g;v) supposing ∀x:T. ((x ∈ v) ⇒ (f x ~ g x))
⊢ [f u / map(f;v)] ~ [g u / map(g;v)] supposing ∀x:T. ((x ∈ [u / v]) ⇒ (f x ~ g x))

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  \msubseteq{}r  Base
3.  f  :  Base
4.  g  :  Base
5.  L  :  T  List
\mvdash{}  map(f;L)  \msim{}  map(g;L)  supposing  \mforall{}x:T.  ((x  \mmember{}  L)  {}\mRightarrow{}  (f  x  \msim{}  g  x))


By

---

Latex:
(ListInd  (-1)  THEN  Reduce  0)

---

Home Index