---

Step * of Lemma iff_weakening_equal

∀[A,B:Type].  {A ⇐⇒ B} supposing A = B ∈ Type
BY
{ (Unfold `guard` 0
   THEN ((UnivCD THENA Auto)
         THEN (RepeatFor 2 (D 0) THENA Auto)
         THEN RenameVar `x' (-1)
         THEN UseWitness ⌜x⌝⋅
         THEN HypReplacementVar
         THEN Eq)
   ) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `guard`  0
  THEN  ((UnivCD  THENA  Auto)
              THEN  (RepeatFor  2  (D  0)  THENA  Auto)
              THEN  RenameVar  `x'  (-1)
              THEN  UseWitness  \mkleeneopen{}x\mkleeneclose{}\mcdot{}
              THEN  HypReplacementVar
              THEN  Eq)
  )

---

Home Index