---

Step * of Lemma equipollent_weakening

∀[A,B:Type].  A ~ B supposing A = B ∈ Type
BY
{ (Unfold `equipollent` 0 THEN Auto THEN HypSubst' -1 0 THEN Auto THEN InstConcl [⌜λx.x⌝]⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    A  \msim{}  B  supposing  A  =  B


By

---

Latex:
(Unfold  `equipollent`  0  THEN  Auto  THEN  HypSubst'  -1  0  THEN  Auto  THEN  InstConcl  [\mkleeneopen{}\mlambda{}x.x\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index