---

Step * 1 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 : f(x)@i
⊢ x1@0 ∈ g(x)
BY
{ (DoSubsume THEN Auto THEN SubtypeRelEq) }

1
.....equality..... 
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 : f(x)@i
11. x1@0 = x1@0 ∈ f(x)
⊢ f(x) = g(x) ∈ Type

---

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.  \muparrow{}x  \mmember{}  dom(f)
9.  \muparrow{}x  \mmember{}  dom(g)
10.  x1@0  :  f(x)@i
\mvdash{}  x1@0  \mmember{}  g(x)


By

(DoSubsume  THEN  Auto  THEN  SubtypeRelEq)

---

Home Index