---

Step * 1 1 of Lemma eo-record-record-eq


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'
4. r."E" ∈ Type
5. x:Atom ─→ if x =a "E" then Type
             if x =a "dom" then r."E" ─→ 𝔹
             if x =a "<" then r."E" ─→ r."E" ─→ ℙ
             if x =a "locless" then r."E" ─→ r."E" ─→ 𝔹
             if x =a "loc" then r."E" ─→ Id
             if x =a "pred" then r."E" ─→ r."E"
             if x =a "rank" then r."E" ─→ ℕ
             else Top
             fi  ∈ 𝕌'
6. r'."E" = r."E" ∈ Type
⊢ r' = r ∈ eo_record{i:l}()
BY
{ (Symmetry
   THEN (RepUR ``record eo-record-type`` 3 THEN RecordExt)
   THEN Try (Trivial)
   THEN Try (\p. let T,x,y = dest_equal (concl p) in
                      let z = subtermn 2 x in
                      (RepUR ``record-select`` 0
                       THEN At ⌈𝕌'⌉ (ApFunToHypEquands `Z' (subst [`a',z] ⌈Z a⌉) T 3)⋅
                       THEN Try (Trivial)
                       THEN Try ((Unfold `record-select` -1 THEN Trivial))
                       THEN Fold `member` 0
                       THEN (DoSubsume THENL [Auto; (Reduce 0 THEN Auto)])) p⋅)) }

1
.....wf..... 
1. r : eo_record{i:l}()@i'
2. r' : record(x.eo-record-type{i:l}(r) x)@i'
3. r'
= r
∈ (x:Atom ─→ if x =a "E" then Type
             if x =a "dom" then r."E" ─→ 𝔹
             if x =a "<" then r."E" ─→ r."E" ─→ ℙ
             if x =a "locless" then r."E" ─→ r."E" ─→ 𝔹
             if x =a "loc" then r."E" ─→ Id
             if x =a "pred" then r."E" ─→ r."E"
             if x =a "rank" then r."E" ─→ ℕ
             else Top
             fi )@i'
4. r."E" ∈ Type
5. x:Atom ─→ if x =a "E" then Type
             if x =a "dom" then r."E" ─→ 𝔹
             if x =a "<" then r."E" ─→ r."E" ─→ ℙ
             if x =a "locless" then r."E" ─→ r."E" ─→ 𝔹
             if x =a "loc" then r."E" ─→ Id
             if x =a "pred" then r."E" ─→ r."E"
             if x =a "rank" then r."E" ─→ ℕ
             else Top
             fi  ∈ 𝕌'
6. r'."E" = r."E" ∈ Type
7. r ∈ eo_record{i:l}()
⊢ r' ∈ eo_record{i:l}()

---

Latex:



1.  r  :  eo\_record\{i:l\}()@i'
2.  r'  :  record(x.eo-record-type\{i:l\}(r)  x)@i'
3.  r'  =  r@i'
4.  r."E"  \mmember{}  Type
5.  x:Atom  {}\mrightarrow{}  if  x  =a  "E"  then  Type
                          if  x  =a  "dom"  then  r."E"  {}\mrightarrow{}  \mBbbB{}
                          if  x  =a  "<"  then  r."E"  {}\mrightarrow{}  r."E"  {}\mrightarrow{}  \mBbbP{}
                          if  x  =a  "locless"  then  r."E"  {}\mrightarrow{}  r."E"  {}\mrightarrow{}  \mBbbB{}
                          if  x  =a  "loc"  then  r."E"  {}\mrightarrow{}  Id
                          if  x  =a  "pred"  then  r."E"  {}\mrightarrow{}  r."E"
                          if  x  =a  "rank"  then  r."E"  {}\mrightarrow{}  \mBbbN{}
                          else  Top
                          fi    \mmember{}  \mBbbU{}'
6.  r'."E"  =  r."E"
\mvdash{}  r'  =  r


By

(Symmetry
  THEN  (RepUR  ``record  eo-record-type``  3  THEN  RecordExt)
  THEN  Try  (Trivial)
  THEN  Try  (\mbackslash{}p.  let  T,x,y  =  dest\_equal  (concl  p)  in
                                        let  z  =  subtermn  2  x  in
                                        (RepUR  ``record-select``  0
                                          THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (ApFunToHypEquands  `Z'  (subst  [`a',z]  \mkleeneopen{}Z  a\mkleeneclose{})  T  3)\mcdot{}
                                          THEN  Try  (Trivial)
                                          THEN  Try  ((Unfold  `record-select`  -1  THEN  Trivial))
                                          THEN  Fold  `member`  0
                                          THEN  (DoSubsume  THENL  [Auto;  (Reduce  0  THEN  Auto)]))  p\mcdot{}))

---

Home Index