---

Step * 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'
⊢ r' = r ∈ eo_record{i:l}()
BY
{ ((Assert r."E" ∈ Type BY
          (DRecord 1 THEN Auto))
   THEN (Assert 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  ∈ 𝕌' BY
               Auto)
   THEN (Assert r'."E" = r."E" ∈ Type BY
               \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 Fold `member` 0
                         THEN (DoSubsume THENL [Auto; (Reduce 0 THEN Auto)])) p⋅)) }

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'
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}()

---

Latex:

---

Latex:

1.  r  :  eo\_record\{i:l\}()@i'
2.  r'  :  record(x.eo-record-type\{i:l\}(r)  x)@i'
3.  r'  =  r@i'
\mvdash{}  r'  =  r


By

---

Latex:
((Assert  r."E"  \mmember{}  Type  BY
                (DRecord  1  THEN  Auto))
  THEN  (Assert  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{}'  BY
                          Auto)
  THEN  (Assert  r'."E"  =  r."E"  BY
                          \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  Fold  `member`  0
                                              THEN  (DoSubsume  THENL  [Auto;  (Reduce  0  THEN  Auto)]))  p\mcdot{}))

---

Home Index