U (lemma)
ub_opp [in ub_opp]
ub_to_lub [in ub_to_lub]
ub_lt_2_pos [in ub_lt_2_pos]
UIP_refl__Streicher_K [in UIP_refl__Streicher_K]
UIP_refl_refl [in UIP_refl_refl]
UIP_dec [in UIP_dec]
UIP__UIP_refl [in UIP__UIP_refl]
UL_sequence [in UL_sequence]
unfold_Stream [in unfold_Stream]
Union_commutative [in Union_commutative]
union_empty_right [in union_empty_right]
Union_absorbs [in Union_absorbs]
Union_is_Lub [in Union_is_Lub]
Union_preserves_Finite [in Union_preserves_Finite]
union_empty_left [in union_empty_left]
Union_minimal [in Union_minimal]
Union_increases_l [in Union_increases_l]
Union_increases_r [in Union_increases_r]
Union_associative [in Union_associative]
union_ass [in union_ass]
union_rotate [in union_rotate]
union_perm_left [in union_perm_left]
Union_inv [in Union_inv]
Union_add [in Union_add]
union_comm [in union_comm]
Union_idempotent [in Union_idempotent]
uniqueness_step3 [in uniqueness_step3]
uniqueness_sum [in uniqueness_sum]
uniqueness_step1 [in uniqueness_step1]
uniqueness_limite [in uniqueness_limite]
uniqueness_step2 [in uniqueness_step2]
unique_existence [in unique_existence]
unique_choice [in unique_choice]
unique_choice [in unique_choice]
uniset_twist1 [in uniset_twist1]
uniset_twist2 [in uniset_twist2]
Un_cv_crit_lub [in Un_cv_crit_lub]
Un_bound_imp [in Un_bound_imp]
Un_in_EUn [in Un_in_EUn]
Un_cv_crit [in Un_cv_crit]
Un_cv_ext [in Un_cv_ext]
Update_WSets.subset_spec [in subset_spec]
Update_WSets.remove_spec [in remove_spec]
Update_WSets.exists_spec [in exists_spec]
Update_WSets.equal_spec [in equal_spec]
Update_WSets.singleton_spec [in singleton_spec]
Update_OT.compare_spec [in compare_spec]
Update_Sets.compare_spec [in compare_spec]
Update_WSets.add_spec [in add_spec]
Update_WSets.mem_spec [in mem_spec]
Update_WSets.is_empty_spec [in is_empty_spec]
Update_WSets.elements_spec1 [in elements_spec1]
Update_WSets.for_all_spec [in for_all_spec]
up_tech [in up_tech]
UsualMinMaxDecProperties.max_dec [in max_dec]
UsualMinMaxDecProperties.max_case_strong [in max_case_strong]
UsualMinMaxDecProperties.max_case [in max_case]
UsualMinMaxDecProperties.min_case [in min_case]
UsualMinMaxDecProperties.min_case_strong [in min_case_strong]
UsualMinMaxDecProperties.min_dec [in min_dec]
UsualMinMaxLogicalProperties.max_min_antimonotone [in max_min_antimonotone]
UsualMinMaxLogicalProperties.max_monotone [in max_monotone]
UsualMinMaxLogicalProperties.min_monotone [in min_monotone]
UsualMinMaxLogicalProperties.min_max_antimonotone [in min_max_antimonotone]