---

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


1. A : Type
2. B : Base
3. base-type-family{i:l}(A;a.B[a])
4. f : Base
5. g : Base
6. h : Base
7. ∀[a,b:Base].  (f a) = (g b) ∈ B[a] supposing a = b ∈ A
8. ∀[a,b:Base].  (g a) = (h b) ∈ B[a] supposing a = b ∈ A
9. a : Base
10. b : Base
11. a = b ∈ A
12. ∀a:A. (B[a] ∈ Type)
13. (f a) = (g b) ∈ B[a]
14. (g b) = (h b) ∈ B[b]
⊢ (f a) = (h b) ∈ B[a]
BY
{ (Assert B[a] = B[b] ∈ Type BY
         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. h : Base
7. ∀[a,b:Base].  (f a) = (g b) ∈ B[a] supposing a = b ∈ A
8. ∀[a,b:Base].  (g a) = (h b) ∈ B[a] supposing a = b ∈ A
9. a : Base
10. b : Base
11. a = b ∈ A
12. ∀a:A. (B[a] ∈ Type)
13. (f a) = (g b) ∈ B[a]
14. (g b) = (h b) ∈ B[b]
15. B[a] = B[b] ∈ Type
⊢ (f a) = (h b) ∈ B[a]

---

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.  h  :  Base
7.  \mforall{}[a,b:Base].    (f  a)  =  (g  b)  supposing  a  =  b
8.  \mforall{}[a,b:Base].    (g  a)  =  (h  b)  supposing  a  =  b
9.  a  :  Base
10.  b  :  Base
11.  a  =  b
12.  \mforall{}a:A.  (B[a]  \mmember{}  Type)
13.  (f  a)  =  (g  b)
14.  (g  b)  =  (h  b)
\mvdash{}  (f  a)  =  (h  b)


By

---

Latex:
(Assert  B[a]  =  B[b]  BY
              Auto)

---

Home Index