---

Step * of Lemma es-interface-equality-prior-recursion

∀[Info,T:Type]. ∀[X,Y:EClass(T)].
  X = Y ∈ EClass(T) 
  supposing ∀es:EO+(Info). ∀e:E.  ((((X)' es e) = ((Y)' es e) ∈ bag(T)) ⇒ ((X es e) = (Y es e) ∈ bag(T)))
BY
{ (Auto THEN (BLemma `es-interface-equality-recursion` ⋅ THEN Auto THEN BHyp -4  THEN Auto)⋅) }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Y : EClass(T)
5. ∀es:EO+(Info). ∀e:E.  ((((X)' es e) = ((Y)' es e) ∈ bag(T)) ⇒ ((X es e) = (Y es e) ∈ bag(T)))
6. es : EO+(Info)@i'
7. e : E@i
8. ∀e':E. ((e' < e) ⇒ ((X es e') = (Y es e') ∈ bag(T)))@i
⊢ ((X)' es e) = ((Y)' es e) ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[X,Y:EClass(T)].
    X  =  Y  supposing  \mforall{}es:EO+(Info).  \mforall{}e:E.    ((((X)'  es  e)  =  ((Y)'  es  e))  {}\mRightarrow{}  ((X  es  e)  =  (Y  es  e)))


By

---

Latex:
(Auto  THEN  (BLemma  `es-interface-equality-recursion`  \mcdot{}  THEN  Auto  THEN  BHyp  -4    THEN  Auto)\mcdot{})

---

Home Index