---

Step * 2 of Lemma es-interval-one-one


1. es : EO
2. d : E
3. b : E
4. a : E
5. c : E
6. a ≤loc b 
7. c ≤loc d 
8. [a, b] = [c, d] ∈ (E List)
9. a = c ∈ E
⊢ {(a = c ∈ E) ∧ (b = d ∈ E)}
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN (RevHypSubst (-1) (-2))
   THEN Auto
   THEN (Using [`a',a] (BLemma `es-interval-length-one-one`))⋅
   THEN Auto) }

---

Latex:



1.  es  :  EO
2.  d  :  E
3.  b  :  E
4.  a  :  E
5.  c  :  E
6.  a  \mleq{}loc  b 
7.  c  \mleq{}loc  d 
8.  [a,  b]  =  [c,  d]
9.  a  =  c
\mvdash{}  \{(a  =  c)  \mwedge{}  (b  =  d)\}


By

(Unfold  `guard`  0
  THEN  Auto
  THEN  (RevHypSubst  (-1)  (-2))
  THEN  Auto
  THEN  (Using  [`a',a]  (BLemma  `es-interval-length-one-one`))\mcdot{}
  THEN  Auto)

---

Home Index