---

Step * 2 of Lemma subtype-fpf-cap-top


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. g ⊆ f
8. ¬↑x ∈ dom(f)
9. ↑x ∈ dom(g)
10. x1@0 : T@i
⊢ x1@0 ∈ g(x)
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.  g  \msubseteq{}  f
8.  \mneg{}\muparrow{}x  \mmember{}  dom(f)
9.  \muparrow{}x  \mmember{}  dom(g)
10.  x1@0  :  T@i
\mvdash{}  x1@0  \mmember{}  g(x)


By

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

---

Home Index