---

Step * of Lemma global-eo-eq-E

∀[L:(Id × Top) List]. ∀[a,b:E].  (a = b ~ (a =z b))
BY
{ (Intros
   THEN Try ((RWO "global-eo-E-sq" 0 THEN Auto))
   THEN (All (RWO "global-eo-E-sq") THENA Auto)
   THEN (Assert ⌜a = b = (a =z b)⌝⋅ THENM (HypSubst' (-1) 0 THEN Auto))) }

1
.....assertion..... 
1. L : (Id × Top) List
2. a : {e:ℕ||L||| True} 
3. b : {e:ℕ||L||| True} 
⊢ a = b = (a =z b)

---

Latex:

---

Latex:
\mforall{}[L:(Id  \mtimes{}  Top)  List].  \mforall{}[a,b:E].    (a  =  b  \msim{}  (a  =\msubz{}  b))


By

---

Latex:
(Intros
  THEN  Try  ((RWO  "global-eo-E-sq"  0  THEN  Auto))
  THEN  (All  (RWO  "global-eo-E-sq")  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}a  =  b  =  (a  =\msubz{}  b)\mkleeneclose{}\mcdot{}  THENM  (HypSubst'  (-1)  0  THEN  Auto)))

---

Home Index