---

Step * of Lemma function-eq-transitivity

∀[A:Type]. ∀[B:Base].
  ∀[f,g,h:Base].  (function-eq(A;a.B[a];f;g) ⇒ function-eq(A;a.B[a];g;h) ⇒ function-eq(A;a.B[a];f;h)) 
  supposing base-type-family{i:l}(A;a.B[a])
BY
{ (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. 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
⊢ (f a) = (h b) ∈ B[a]

---

Latex:

---

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


By

---

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

---

Home Index