---

Step * of Lemma equipollent_functionality_wrt_ext-eq-left

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

---

Latex:

---

Latex:
\mforall{}[A1,A2,B1,B2:Type].    (A1  \msim{}  B1  \mLeftarrow{}{}\mRightarrow{}  A2  \msim{}  B2)  supposing  ((B1  =  B2)  and  A1  \mequiv{}  A2)


By

---

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

---

Home Index