---

Step * 1 1 1 of Lemma function-eq-implies


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. a1 : Base
8. b : Base
9. c : a1 = b ∈ A
10. ∀a:A. (B[a] ∈ Type)
11. B[a1] ∈ Type
⊢ ((f a1) = (g a1) ∈ B[a1]) = ((f b) = (g b) ∈ B[b]) ∈ Type
BY
{ (Assert ⌜B[a1] = B[b] ∈ Type⌝⋅ 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. a1 : Base
8. b : Base
9. c : a1 = b ∈ A
10. ∀a:A. (B[a] ∈ Type)
11. B[a1] ∈ Type
12. B[a1] = B[b] ∈ Type
⊢ ((f a1) = (g a1) ∈ B[a1]) = ((f b) = (g b) ∈ B[b]) ∈ Type

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Base
3.  base-type-family\{i:l\}(A;a.B[a])
4.  f  :  Base
5.  g  :  Base
6.  \mforall{}[a,b:Base].    (f  a)  =  (g  b)  supposing  a  =  b
7.  a1  :  Base
8.  b  :  Base
9.  c  :  a1  =  b
10.  \mforall{}a:A.  (B[a]  \mmember{}  Type)
11.  B[a1]  \mmember{}  Type
\mvdash{}  ((f  a1)  =  (g  a1))  =  ((f  b)  =  (g  b))


By

---

Latex:
(Assert  \mkleeneopen{}B[a1]  =  B[b]\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index