---

Step * of Lemma es-E-equality-univ-independent

∀[es:EO]. ∀[e,e':E].
  (TERMOF{decidable__es-E-equal:o, 1:l, i:l} es e' e ~ TERMOF{decidable__es-E-equal:o, 1:l, 1:l} es e' e)
BY
{ ((UnivCD THENA Auto)
   THEN RW (SubC (ComputeToC [])) 0
   THEN Reduce 0
   THEN Repeat ((RW (SubC (ComputeToC [])) 0 THEN Reduce 0 THEN EqCD))) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].
    (TERMOF\{decidable\_\_es-E-equal:o,  1:l,  i:l\}  es  e'  e  \msim{}  TERMOF\{decidable\_\_es-E-equal:o,  1:l,  1:l\}  es 
                                                                                                              e' 
                                                                                                              e)


By

((UnivCD  THENA  Auto)
  THEN  RW  (SubC  (ComputeToC  []))  0
  THEN  Reduce  0
  THEN  Repeat  ((RW  (SubC  (ComputeToC  []))  0  THEN  Reduce  0  THEN  EqCD)))

---

Home Index