---

Step * 2 1 1 1 1 2 of Lemma eo-forward-trivial

.....set predicate..... 
1. v : eo_record{i:l}()@i'
2. eo_axioms(v)@i'
⊢ eo_axioms(v["dom" := v."dom"])
BY
{ (All (RepUR ``eo_axioms``) THEN Trivial) }

---

Latex:


.....set  predicate..... 
1.  v  :  eo\_record\{i:l\}()@i'
2.  eo\_axioms(v)@i'
\mvdash{}  eo\_axioms(v["dom"  :=  v."dom"])


By

(All  (RepUR  ``eo\_axioms``)  THEN  Trivial)

---

Home Index