---

Step * 1 1 of Lemma es-dt-dom


1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
⊢ ↑tg ∈ dom(dt(l;da)) ⇐⇒ ↑rcv(l,tg) ∈ dom(da)
BY
{ ((RWO "member-fpf-domain" 0 THENA Auto)
   THEN Unfold `es-dt` 0
   THEN RWO "compose-fpf-dom" 0
   THEN Try (Complete (Auto))) }

1
1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
⊢ ∃x:Knd
   ((x ∈ fpf-domain(da))
   ∧ ((↑isl((λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ) x))
     c∧ (tg = outl((λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ) x) ∈ Id)))
⇐⇒ (rcv(l,tg) ∈ fpf-domain(da))

2
.....wf..... 
1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
4. -any : ∃x:Knd
           ((x ∈ fpf-domain(da))
           ∧ ((↑isl((λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ) x))
             c∧ (tg
                = outl((λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ) x)
                ∈ Id))) ∈ Type
⊢ (tg
    ∈ fpf-domain(compose-fpf(λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ;...;da)))
  ∈ Type

3
.....wf..... 
1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
4. ∃x:Knd
    ((x ∈ fpf-domain(da))
    ∧ ((↑isl((λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ) x))
      c∧ (tg = outl((λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ) x) ∈ Id)))
⇐⇒ (rcv(l,tg) ∈ fpf-domain(da))
⊢ ∃x:Knd
   ((x ∈ fpf-domain(da))
   ∧ ((↑isl((λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ) x))
     c∧ (tg = outl((λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ) x) ∈ Id)))
  ⇐⇒ (rcv(l,tg) ∈ fpf-domain(da)) ∈ Type

---

Latex:



1.  l  :  IdLnk@i
2.  da  :  k:Knd  fp->  Type@i'
3.  tg  :  Id@i
\mvdash{}  \muparrow{}tg  \mmember{}  dom(dt(l;da))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}rcv(l,tg)  \mmember{}  dom(da)


By

((RWO  "member-fpf-domain"  0  THENA  Auto)
  THEN  Unfold  `es-dt`  0
  THEN  RWO  "compose-fpf-dom"  0
  THEN  Try  (Complete  (Auto)))

---

Home Index