---

Step * of Lemma function-eq-symmetry

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

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 : Base
8. b : Base
9. a = b ∈ A
⊢ (f b) = (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{}  function-eq(A;a.B[a];g;f)) 
    supposing  base-type-family\{i:l\}(A;a.B[a])


By

---

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

---

Home Index