---

Step * of Lemma prior-latest-val

∀[Info,T:Type]. ∀[X:EClass(T)].  (((X)-)' = (X)' ∈ EClass(T))
BY
{ Auto
THEN Symmetry
THEN ((BLemma `es-interface-extensionality` THENA Auto) THEN Try (Complete ((ProveSV THEN Auto)))) }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
⊢ ∀es:EO+(Info). ∀e:E.  (↑e ∈b (X)' ⇐⇒ ↑e ∈b ((X)-)')

2
1. Info : Type
2. T : Type
3. X : EClass(T)
⊢ ∀es:EO+(Info). ∀e:E.  ((↑e ∈b (X)') ⇒ (↑e ∈b ((X)-)') ⇒ ((X)'(e) = ((X)-)'(e) ∈ T))

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].    (((X)\msupminus{})'  =  (X)')


By

---

Latex:
Auto
THEN  Symmetry
THEN  ((BLemma  `es-interface-extensionality`  THENA  Auto)  THEN  Try  (Complete  ((ProveSV  THEN  Auto))))

---

Home Index