---

Step * of Lemma in-bar-converges

∀[T:Type]. ∀[b,a:T].  (in-bar(a)↓b ⇐⇒ a = b ∈ T)
BY
{ ((D 0 THENA Auto)
   THEN (Assert ∀[b:T]. in-bar(b)↓b BY
               (Auto THEN With ⌜0⌝ (D 0)⋅ THEN Auto THEN SymbolicCompute [] [] [2] 0 THEN Auto))
   THEN Auto
   THEN InstHyp [⌜a⌝] 2⋅
   THEN Auto
   THEN FLemma `bar-converges-unique` [-2;-1]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b,a:T].    (in-bar(a)\mdownarrow{}b  \mLeftarrow{}{}\mRightarrow{}  a  =  b)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  \mforall{}[b:T].  in-bar(b)\mdownarrow{}b  BY
                          (Auto  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  SymbolicCompute  []  []  [2]  0  THEN  Auto))
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  2\mcdot{}
  THEN  Auto
  THEN  FLemma  `bar-converges-unique`  [-2;-1]
  THEN  Auto)

---

Home Index