---

Step * 1 2 of Lemma map_functionality_wrt_sq


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))
BY
{ TACTIC:(D 0 THENA Auto) }

1
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))
8. ∀x:T. ((x ∈ [u / v]) ⇒ (f x ~ g x))
⊢ [f u / map(f;v)] ~ [g u / map(g;v)]

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  \msubseteq{}r  Base
3.  f  :  Base
4.  g  :  Base
5.  u  :  T
6.  v  :  T  List
7.  map(f;v)  \msim{}  map(g;v)  supposing  \mforall{}x:T.  ((x  \mmember{}  v)  {}\mRightarrow{}  (f  x  \msim{}  g  x))
\mvdash{}  [f  u  /  map(f;v)]  \msim{}  [g  u  /  map(g;v)]  supposing  \mforall{}x:T.  ((x  \mmember{}  [u  /  v])  {}\mRightarrow{}  (f  x  \msim{}  g  x))


By

---

Latex:
TACTIC:(D  0  THENA  Auto)

---

Home Index