Step * 1 1 of Lemma list_of_extensions_in_fin_spr1


1. B :  List  @i
2. b :  List@i
3. a :  List@i
4. (b  fspr(B))
 (b  fspr(B)) ~ tt
BY
{ MaAuto }



1.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  b  :  \mBbbN{}  List@i
3.  a  :  \mBbbN{}  List@i
4.  \muparrow{}(b  \mmember{}  fspr(B))
\mvdash{}  (b  \mmember{}  fspr(B))  \msim{}  tt


By

MaAuto



Home Index