Require Export tbs_fun.

Section Subset_Finite_Definitions.

   Section subsets_from_lists.

      Definition SList: (S:Set) (List S) -> (S -> Set) := [S](ListFam S [_](S->Set) (SBot S) [_;p;a](SOr S p (Sing S a))).

   End subsets_from_lists.

   Section subset_finite_predicate.

      Definition WFin: (S:Set) (S -> Set) -> Set := [S;U](LEx (FDF S) [z](SbE S U (FDFImg S z))).
(*      
Definition SFin: (S:Set) (S -> Set) -> Set := [S;U](Ex (FDF S) [z](SEq S U (FDFImg S z))).
*)
   End subset_finite_predicate.
(*
Section subset_finite_quantification.
   
Definition FAll: (S:Set) ((Part S) -> Set) -> Set := [S;P](z:(FDF S))(P (SFImg S z)).
      
Definition FEx: (S:Set) ((Part S) -> Set) -> Set := [S;P](Ex (FDF S) [z](P (SFImg S z))).
   
End subset_finite_quantification.
*)
End Subset_Finite_Definitions.

Section Subset_Finite_Results.

   Section subset_list.

      Theorem slist_eps_i: (S:Set; a:S; l:(List S)) (LIn S a l) -> (Eps S a (SList S l)).
      Intros S a l.
      MElim l listrec.
      MCut Empty.
      Apply (lin_e S a (empty S)).
      Assumption.
      Intros v w.
      MElim w listrec.
      MApply '(list_p4 S v a).
      MApply '(list_p4 S (app S (fr S v a) l0) s).
      MElim H0 efq.
      Apply (lin_e S a (fr S l0 s)).
      Assumption.
      Intros v w.
      MElim w listrec.
      MApply 'sor_eps_i1.
      MApply 'sing_eps_i.
      MApply '(fr_ini2 S l0 v).
      MApply 'sor_eps_i2.
      MApply 'H.
      MApply '(lin_i S v l1).
      MApply '(fr_ini1 S s0 s).
      Qed.


      Theorem slist_xfdfl: (S:Set; n:N; v:(Fin n)->S) (SbE S (Img (Fin n) S v) (SList S (xfdf_list S n v))).
      Intros.
      MApply 'sbe_i.
      MApply 'slist_eps_i.
      MApply '(img_eps_e (Fin n) S v a).
      MApply '(id_repl S a (v i)).
      MApply 'xfdfl_lin.
      Qed.

      Theorem slist_fdfl: (S:Set; v:(FDF S)) (SbE S (FDFImg S v) (SList S (fdfl S v))).
      Intros.
      MApply '(id_repl (List S) (fdfl S v) (xfdf_list S (fdf_n S v) (fdf_f S v))).
      MElim 'v '(fdf_e S).
      Unfold FDFImg.
      MApply 'slist_xfdfl.
      Qed.

   End subset_list.
   
   Section weakly_finite.

      Theorem wfin_i: (S:Set; v:(FDF S); U:S->Set) (SbE S U (FDFImg S v)) -> (WFin S U).
      Intros.
      Unfold WFin.
      MApply '(lex_i (FDF S) v).
      Qed.
      
      Theorem wfin_e: (S:Set; U:S->Set; P:Set) (WFin S U) -> ((v:(FDF S)) (SbE S U (FDFImg S v)) -> P) -> P.
      Intros.
      MElim 'H 'lex_e.
      MApply '(H0 a).
      Qed.

      Theorem wfin_sand: (S:Set; U,V:S->Set) (WFin S U) -> (WFin S (SAnd S U V)).
      Intros.
      MApply '(wfin_e S U).
      MApply '(wfin_i S v).
      MApply '(sbe_t S U).
      MApply 'sand_sbe_e2.
      Qed.

      Theorem wfin_sor: (S:Set; U,V:S->Set) (WFin S U) -> (WFin S V) -> (WFin S (SOr S U V)).
      Intros.
      MApply '(wfin_e S U).
      MApply '(wfin_e S V).
      MApply '(wfin_i S (fdf_add S v v0)).
      MApply '(sbe_t S (SOr S (FDFImg S v) (FDFImg S v0))).
      MApply 'sor_sbe_c.
      MApply 'img_fdf_add_i.
      Qed.

      Theorem wfin_list: (S:Set; U:S->Set) (WFin S U) -> (LEx (List S) [v](SbE S U (SList S v))). 
      Intros.
      MApply '(wfin_e S U).
      MApply '(lex_i (List S) (fdfl S v)).
      MApply '(sbe_t S (FDFImg S v)).
      MApply 'slist_fdfl.
      Qed.      

   End weakly_finite.

End Subset_Finite_Results.