---

Step * of Lemma function-eq-symmetry-type-function

∀A:Type. ∀B:type-function{i:l}(A). ∀f,g:Base.  (function-eq(A;a.B[a];f;g) ⇒ function-eq(A;a.B[a];g;f))
BY
{ RepeatFor 4 (Intro) }

1
1. A : Type@i'
2. B : type-function{i:l}(A)@i'
3. f : Base@i
4. g : Base@i
⊢ function-eq(A;a.B[a];f;g) ⇒ function-eq(A;a.B[a];g;f)

---

Latex:

---

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


By

---

Latex:
RepeatFor  4  (Intro)

---

Home Index