---

Step * of Lemma map_functionality_wrt_sq

∀[T:Type]. ∀[f,g:Base]. ∀[L:T List].  map(f;L) ~ map(g;L) supposing ∀x:T. ((x ∈ L) ⇒ (f x ~ g x)) supposing T ⊆r Base
BY
{ TACTIC:RepeatFor 5 ((D 0 THENA Auto)) }

1
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))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[f,g:Base].  \mforall{}[L:T  List].    map(f;L)  \msim{}  map(g;L)  supposing  \mforall{}x:T.  ((x  \mmember{}  L)  {}\mRightarrow{}  (f  x  \msim{}  g  x)) 
    supposing  T  \msubseteq{}r  Base


By

---

Latex:
TACTIC:RepeatFor  5  ((D  0  THENA  Auto))

---

Home Index