---

Step * of Lemma update_wf

∀[A,B:Type]. ∀[eq:A ⟶ A ⟶ 𝔹]. ∀[f:A ⟶ B]. ∀[x:A]. ∀[v:B].  (f[x:=v] ∈ A ⟶ B)
BY
{ (Unfold `update` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[eq:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[x:A].  \mforall{}[v:B].    (f[x:=v]  \mmember{}  A  {}\mrightarrow{}  B)


By

---

Latex:
(Unfold  `update`  0  THEN  Auto)

---

Home Index