---

Step * of Lemma function_functionality_wrt_equipollent

∀[A:Type]. ∀[B,C:A ⟶ Type].  ((∀a:A. B[a] ~ C[a]) ⇒ a:A ⟶ B[a] ~ a:A ⟶ C[a])
BY
{ (Auto THEN Unfold `equipollent` -1 THEN (Skolemize (-1) `F' THENA Auto) THEN (D 0 With ⌜λf,a. (F a (f a))⌝  THENA Auto\000C)) }

1
1. [A] : Type
2. [B] : A ⟶ Type
3. [C] : A ⟶ Type
4. ∀a:A. ∃f:B[a] ⟶ C[a]. Bij(B[a];C[a];f)
5. F : a:A ⟶ B[a] ⟶ C[a]
6. ∀a:A. Bij(B[a];C[a];F a)
⊢ Bij(a:A ⟶ B[a];a:A ⟶ C[a];λf,a. (F a (f a)))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B,C:A  {}\mrightarrow{}  Type].    ((\mforall{}a:A.  B[a]  \msim{}  C[a])  {}\mRightarrow{}  a:A  {}\mrightarrow{}  B[a]  \msim{}  a:A  {}\mrightarrow{}  C[a])


By

---

Latex:
(Auto
  THEN  Unfold  `equipollent`  -1
  THEN  (Skolemize  (-1)  `F'  THENA  Auto)
  THEN  (D  0  With  \mkleeneopen{}\mlambda{}f,a.  (F  a  (f  a))\mkleeneclose{}    THENA  Auto))

---

Home Index