---

Step * of Lemma function-eq-implies

∀[A:Type]. ∀[B:Base].
  ∀[f,g:Base].  (function-eq(A;a.B[a];f;g) ⇒ {∀[a:A]. ((f a) = (g a) ∈ B[a])}) 
  supposing base-type-family{i:l}(A;a.B[a])
BY
{ (Unfold `guard` 0 THEN Auto THEN All (Unfold `function-eq`) THEN Auto) }

1
1. A : Type
2. B : Base
3. base-type-family{i:l}(A;a.B[a])
4. f : Base
5. g : Base
6. ∀[a,b:Base].  (f a) = (g b) ∈ B[a] supposing a = b ∈ A
7. a : A
⊢ (f a) = (g a) ∈ B[a]

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:Base].
    \mforall{}[f,g:Base].    (function-eq(A;a.B[a];f;g)  {}\mRightarrow{}  \{\mforall{}[a:A].  ((f  a)  =  (g  a))\}) 
    supposing  base-type-family\{i:l\}(A;a.B[a])


By

---

Latex:
(Unfold  `guard`  0  THEN  Auto  THEN  All  (Unfold  `function-eq`)  THEN  Auto)

---

Home Index