---

Step * 1 1 of Lemma map_functionality_wrt_sq


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

---

Latex:

---

Latex:

1.  T  :  Type
2.  T  \msubseteq{}r  Base
3.  f  :  Base
4.  g  :  Base
\mvdash{}  []  \msim{}  []  supposing  \mforall{}x:T.  ((x  \mmember{}  [])  {}\mRightarrow{}  (f  x  \msim{}  g  x))


By

---

Latex:
Auto

---

Home Index