---

Step * of Lemma stable__function_equal

∀[A,B:Type]. ∀[f,g:A ⟶ B].  Stable{f = g ∈ (A ⟶ B)} supposing ∀x:A. Stable{(f x) = (g x) ∈ B}
BY
{ (Unfold `stable` 0 THEN Auto THEN FunExt THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f,g:A  {}\mrightarrow{}  B].    Stable\{f  =  g\}  supposing  \mforall{}x:A.  Stable\{(f  x)  =  (g  x)\}


By

---

Latex:
(Unfold  `stable`  0  THEN  Auto  THEN  FunExt  THEN  Auto)

---

Home Index