---

Step * 1 of Lemma subtype-fpf-cap-void


1. T : Type
2. X : Type
3. eq : EqDecider(X)
4. f : x:X fp-> Type
5. g : x:X fp-> Type
6. x : X
7. f ⊆ g
8. ↑x ∈ dom(f)
9. ¬↑x ∈ dom(g)
10. x1 : f(x)@i
⊢ x1 ∈ T
BY
{ ((Unfold `fpf-sub` (-4)) THEN (InstHyp [⌈x⌉] (-4))⋅ THEN ExRepD THEN Auto) }

---

Latex:



1.  T  :  Type
2.  X  :  Type
3.  eq  :  EqDecider(X)
4.  f  :  x:X  fp->  Type
5.  g  :  x:X  fp->  Type
6.  x  :  X
7.  f  \msubseteq{}  g
8.  \muparrow{}x  \mmember{}  dom(f)
9.  \mneg{}\muparrow{}x  \mmember{}  dom(g)
10.  x1  :  f(x)@i
\mvdash{}  x1  \mmember{}  T


By

((Unfold  `fpf-sub`  (-4))  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-4))\mcdot{}  THEN  ExRepD  THEN  Auto)

---

Home Index