%--------------------------------------------------------------%
%   Author: Dragan Stosic                                      %
%--------------------------------------------------------------%

relational_choice_properties[T, U: TYPE+]: THEORY
 BEGIN

  IMPORTING relational_choice[T, U]

  fun_choice_impl_description: LEMMA fun_choice IMPLIES parametric_definite_description

  fun_choice_impl_rel_unique_choice: LEMMA fun_choice IMPLIES rel_unique_choice

  fun_choice_impl_rel_choice: LEMMA fun_choice IMPLIES rel_choice

  fun_choice_impl_rel_choice_impl_description_rel_choice: LEMMA
    fun_choice IMPLIES rel_choice IMPLIES parametric_definite_description

  fun_choice_impl_rel_choice_and_description_rel_choice: LEMMA
    fun_choice IMPLIES rel_choice AND parametric_definite_description

  fun_choice_impl_rel_unique_choice_impl_description_rel_choice: LEMMA
    fun_choice IMPLIES rel_unique_choice IMPLIES parametric_definite_description

  fun_choice_impl_rel_unique_choice_and_description_rel_choice: LEMMA
    fun_choice IMPLIES rel_unique_choice AND parametric_definite_description

  description_rel_unique_choice_imp_funct_choice: LEMMA
    parametric_definite_description IMPLIES rel_unique_choice IMPLIES fun_choice

  description_rel_and_rel_unique_choice_imp_funct_choice: LEMMA
    parametric_definite_description AND rel_unique_choice IMPLIES fun_choice

  rel_choice_and_proof_irrel_imp_guarded_rel_choice: LEMMA
    rel_unique_choice IMPLIES proof_irrelevance IMPLIES conditional_relational_choice

  relx_choice_indep_of_premises_imp_guarded_rel_choice: LEMMA
    rel_unique_choice IMPLIES independence_of_premises IMPLIES conditional_relational_choice

  fun_choice_equiv_rel_unique_param_desc: THEOREM
    fun_choice IFF rel_unique_choice AND parametric_definite_description

 END relational_choice_properties