---

Step * of Lemma equipollent_functionality_wrt_ext-eq-right

∀[A,B1,B2:Type].  A ~ B1 ⇐⇒ A ~ B2 supposing B1 ≡ B2
BY
{ (Auto
   THEN Try ((Using [`A1',⌜A⌝;`B1',⌜B1⌝] (BLemma `equipollent_functionality_wrt_ext-eq`)⋅
              THEN Auto
              THEN RelRST
              THEN Auto))
   THEN Try ((Using [`A1',⌜A⌝;`B1',⌜B2⌝] (BLemma `equipollent_functionality_wrt_ext-eq`)⋅
              THEN Auto
              THEN RelRST
              THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A,B1,B2:Type].    A  \msim{}  B1  \mLeftarrow{}{}\mRightarrow{}  A  \msim{}  B2  supposing  B1  \mequiv{}  B2


By

---

Latex:
(Auto
  THEN  Try  ((Using  [`A1',\mkleeneopen{}A\mkleeneclose{};`B1',\mkleeneopen{}B1\mkleeneclose{}]  (BLemma  `equipollent\_functionality\_wrt\_ext-eq`)\mcdot{}
                        THEN  Auto
                        THEN  RelRST
                        THEN  Auto))
  THEN  Try  ((Using  [`A1',\mkleeneopen{}A\mkleeneclose{};`B1',\mkleeneopen{}B2\mkleeneclose{}]  (BLemma  `equipollent\_functionality\_wrt\_ext-eq`)\mcdot{}
                        THEN  Auto
                        THEN  RelRST
                        THEN  Auto)))

---

Home Index