---

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

.....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
BY
{ OnMaybeHyp 7 (\h. ((Unfold `fpf-sub` h) THEN (InstHyp [⌈x⌉] h)⋅ THEN ExRepD THEN Complete (Auto))) }

---

Latex:


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


By

OnMaybeHyp  7  (\mbackslash{}h.  ((Unfold  `fpf-sub`  h)  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h)\mcdot{}  THEN  ExRepD  THEN  Complete  (Auto)))

---

Home Index