---

Step * of Lemma es-dt-dom

∀[l:IdLnk]. ∀[da:k:Knd fp-> Type]. ∀[tg:Id].  uiff(↑tg ∈ dom(dt(l;da));↑rcv(l,tg) ∈ dom(da))
BY
{ ((UniformUnivCD Auto THEN Try (RemoveUiff)) THEN Try (Complete (Auto)) THEN Repeat (MoveToConcl (-1))) }

1
∀l:IdLnk. ∀da:k:Knd fp-> Type. ∀tg:Id.  (↑tg ∈ dom(dt(l;da)) ⇐⇒ ↑rcv(l,tg) ∈ dom(da))

---

Latex:


\mforall{}[l:IdLnk].  \mforall{}[da:k:Knd  fp->  Type].  \mforall{}[tg:Id].    uiff(\muparrow{}tg  \mmember{}  dom(dt(l;da));\muparrow{}rcv(l,tg)  \mmember{}  dom(da))


By

((UniformUnivCD  Auto  THEN  Try  (RemoveUiff))
  THEN  Try  (Complete  (Auto))
  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index