---

Step * of Lemma type-function-eta

∀[A:Type]. ∀[B,C:type-function{i:l}(A)].
  ((B = C ∈ type-function{i:l}(A)) ⇒ ((λx.(B x)) = (λx.(C x)) ∈ type-function{i:l}(A)))
BY
{ (At ⌜𝕌'⌝Intros⋅ THEN Try (Complete (Auto)) THEN All (Unfold `type-function`)) }

1
1. A : Type
2. B : per-function(A;a.Type)
3. C : per-function(A;a.Type)
4. B = C ∈ per-function(A;a.Type)
⊢ (λx.(B x)) = (λx.(C x)) ∈ per-function(A;a.Type)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B,C:type-function\{i:l\}(A)].    ((B  =  C)  {}\mRightarrow{}  ((\mlambda{}x.(B  x))  =  (\mlambda{}x.(C  x))))


By

---

Latex:
(At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}Intros\mcdot{}  THEN  Try  (Complete  (Auto))  THEN  All  (Unfold  `type-function`))

---

Home Index