---

Step * of Lemma eo-record-record-eq

∀r:eo_record{i:l}(). ∀r':record(x.eo-record-type{i:l}(r) x).
  ((r' = r ∈ record(x.eo-record-type{i:l}(r) x)) ⇒ (r' = r ∈ eo_record{i:l}()))
BY
{ (Auto THEN Try ((BLemma `eo-record-record` THEN Auto))) }

1
1. r : eo_record{i:l}()@i'
2. r' : record(x.eo-record-type{i:l}(r) x)@i'
3. r' = r ∈ record(x.eo-record-type{i:l}(r) x)@i'
⊢ r' = r ∈ eo_record{i:l}()

---

Latex:


\mforall{}r:eo\_record\{i:l\}().  \mforall{}r':record(x.eo-record-type\{i:l\}(r)  x).    ((r'  =  r)  {}\mRightarrow{}  (r'  =  r))


By

(Auto  THEN  Try  ((BLemma  `eo-record-record`  THEN  Auto)))

---

Home Index