---

Step * 1 of Lemma cp-ktype_wf


1. cp : i:Id fp-> A:Type
                  × ks:{k:Knd| ↑hasloc(k;i)}  List
                  × typ:{k:Knd| (k ∈ ks)}  ─→ Type
                  × k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A ─→ (Top + Top)
                  × A ─→ k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A
                  × A
2. i : {i:Id| (i ∈ fpf-domain(cp))} 
3. k : {k:Knd| (k ∈ (λi.let A,ks,typ,h,acc,init = cp(i) in ks) i)} 
⊢ let A,ks,typ,h,acc,init = cp(i) in 
  typ k ∈ Type
BY
{ (D -2 THEN D -1 THEN All Reduce THEN MoveToConcl (-1) THEN ( (GenConclAtAddr [2;2;1])⋅ THENA Auto THEN Auto))⋅ }

1
1. cp : i:Id fp-> A:Type
                  × ks:{k:Knd| ↑hasloc(k;i)}  List
                  × typ:{k:Knd| (k ∈ ks)}  ─→ Type
                  × k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A ─→ (Top + Top)
                  × A ─→ k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A
                  × A
2. i : Id
3. (i ∈ fpf-domain(cp))
4. k : Knd
5. v : A:Type
× ks:{k:Knd| ↑hasloc(k;i)}  List
× typ:{k:Knd| (k ∈ ks)}  ─→ Type
× k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A ─→ (Top + Top)
× A ─→ k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A
× A@i'
6. cp(i)
= v
∈ (A:Type
  × ks:{k:Knd| ↑hasloc(k;i)}  List
  × typ:{k:Knd| (k ∈ ks)}  ─→ Type
  × k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A ─→ (Top + Top)
  × A ─→ k:{k:Knd| (k ∈ ks)}  ─→ (typ k) ─→ A
  × A)@i'
⊢ (k ∈ let A,ks,typ,h,acc,init = v in ks) ⇒ (let A,ks,typ,h,acc,init = v in typ k ∈ Type)

---

Latex:



1.  cp  :  i:Id  fp->  A:Type
                                    \mtimes{}  ks:\{k:Knd|  \muparrow{}hasloc(k;i)\}    List
                                    \mtimes{}  typ:\{k:Knd|  (k  \mmember{}  ks)\}    {}\mrightarrow{}  Type
                                    \mtimes{}  k:\{k:Knd|  (k  \mmember{}  ks)\}    {}\mrightarrow{}  (typ  k)  {}\mrightarrow{}  A  {}\mrightarrow{}  (Top  +  Top)
                                    \mtimes{}  A  {}\mrightarrow{}  k:\{k:Knd|  (k  \mmember{}  ks)\}    {}\mrightarrow{}  (typ  k)  {}\mrightarrow{}  A
                                    \mtimes{}  A
2.  i  :  \{i:Id|  (i  \mmember{}  fpf-domain(cp))\} 
3.  k  :  \{k:Knd|  (k  \mmember{}  (\mlambda{}i.let  A,ks,typ,h,acc,init  =  cp(i)  in  ks)  i)\} 
\mvdash{}  let  A,ks,typ,h,acc,init  =  cp(i)  in 
    typ  k  \mmember{}  Type


By

(D  -2
  THEN  D  -1
  THEN  All  Reduce
  THEN  MoveToConcl  (-1)
  THEN  (  (GenConclAtAddr  [2;2;1])\mcdot{}  THENA  Auto  THEN  Auto))\mcdot{}

---

Home Index