---

Step * of Lemma fpf-dom-type2

∀[X,Y:Type]. ∀[eq:EqDecider(Y)]. ∀[f:x:X fp-> Top]. ∀[x:Y].  {x ∈ X supposing ↑x ∈ dom(f)} supposing strong-subtype(X;Y)
BY
{ (Unfold `guard` 0 THEN (InstLemma `fpf-dom-type` []) THEN Trivial) }

---

Latex:


\mforall{}[X,Y:Type].  \mforall{}[eq:EqDecider(Y)].  \mforall{}[f:x:X  fp->  Top].  \mforall{}[x:Y].
    \{x  \mmember{}  X  supposing  \muparrow{}x  \mmember{}  dom(f)\}  supposing  strong-subtype(X;Y)


By

(Unfold  `guard`  0  THEN  (InstLemma  `fpf-dom-type`  [])  THEN  Trivial)

---

Home Index