---

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

.....wf..... 
1. v : eo_record{i:l}()@i'
2. eo_axioms(v)@i'
3. r : eo_record{i:l}()
⊢ eo_axioms(r) ∈ Type
BY
{ Auto }

---

Latex:


.....wf..... 
1.  v  :  eo\_record\{i:l\}()@i'
2.  eo\_axioms(v)@i'
3.  r  :  eo\_record\{i:l\}()
\mvdash{}  eo\_axioms(r)  \mmember{}  Type


By

Auto

---

Home Index