---

Step * of Lemma indep-function_functionality_wrt_equipollent

∀[A,B,C,D:Type].  (A ~ B ⇒ C ~ D ⇒ C ⟶ A ~ D ⟶ B)
BY
{ (Auto
   THEN (InstLemma`function_functionality_wrt_equipollent_right` [⌜A⌝;⌜B⌝;⌜C⌝]⋅ THENA Auto)
   THEN (InstLemma`function_functionality_wrt_equipollent_left` [⌜C⌝;⌜D⌝;⌜B⌝]⋅ THENA Auto)) }

1
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. [D] : Type
5. A ~ B
6. C ~ D
7. C ⟶ A ~ C ⟶ B
8. C ⟶ B ~ D ⟶ B
⊢ C ⟶ A ~ D ⟶ B

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma`function\_functionality\_wrt\_equipollent\_right`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma`function\_functionality\_wrt\_equipollent\_left`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}D\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index