---

Step * of Lemma equal-eo-forward-E

∀[eo:EO]. ∀[e:E]. ∀[e1,e2:E].  uiff(e1 = e2 ∈ E;e1 = e2 ∈ E)
BY
{ (BasicUniformUnivCD Auto
   THEN (Assert eo.e ∈ EO BY
               (BLemma `eo-forward-wf` THEN Auto))
   THEN ((UnivCD THENM D 0 THENM D 0) THENA Auto)) }

1
1. eo : EO
2. e : E
3. eo.e ∈ EO
4. e1 : E
5. e2 : E
6. e1 = e2 ∈ E
⊢ e1 = e2 ∈ E

2
1. eo : EO
2. e : E
3. eo.e ∈ EO
4. e1 : E
5. e2 : E
6. e1 = e2 ∈ E
⊢ e1 = e2 ∈ E

---

Latex:


\mforall{}[eo:EO].  \mforall{}[e:E].  \mforall{}[e1,e2:E].    uiff(e1  =  e2;e1  =  e2)


By

(BasicUniformUnivCD  Auto
  THEN  (Assert  eo.e  \mmember{}  EO  BY
                          (BLemma  `eo-forward-wf`  THEN  Auto))
  THEN  ((UnivCD  THENM  D  0  THENM  D  0)  THENA  Auto))

---

Home Index