---

Step * 1 of Lemma fin_spr_mem_in_fin_spr


1. B :  List  @i
2. f : fin_spr(B)@i
 (f  fspr(B))
BY
{ (Unfold `in_fin_spr` 0 THEN D (-1) THEN Reduce 0 THEN Unhide THEN Auto) }



1.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  f  :  fin\_spr(B)@i
\mvdash{}  (f  \mmember{}  fspr(B))


By

(Unfold  `in\_fin\_spr`  0  THEN  D  (-1)\mcdot{}  THEN  Reduce  0  THEN  Unhide  THEN  Auto)



Home Index