diff options
Diffstat (limited to 'theories/Logic/ChoiceFacts.v')
-rw-r--r-- | theories/Logic/ChoiceFacts.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 8d82bc8e..fb7898c6 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -385,7 +385,7 @@ Qed. Lemma subset_types_imp_guarded_rel_choice_iff_rel_choice : ProofIrrelevance -> (GuardedRelationalChoice <-> RelationalChoice). Proof. - auto decomp using + intuition auto using guarded_rel_choice_imp_rel_choice, rel_choice_and_proof_irrel_imp_guarded_rel_choice. Qed. @@ -439,7 +439,7 @@ Corollary fun_choice_and_indep_general_prem_iff_guarded_fun_choice : FunctionalChoiceOnInhabitedSet /\ IndependenceOfGeneralPremises <-> GuardedFunctionalChoice. Proof. - auto decomp using + intuition auto using guarded_fun_choice_imp_indep_of_general_premises, guarded_fun_choice_imp_fun_choice, fun_choice_and_indep_general_prem_imp_guarded_fun_choice. @@ -480,7 +480,7 @@ Corollary fun_choice_and_small_drinker_iff_omniscient_fun_choice : FunctionalChoiceOnInhabitedSet /\ SmallDrinker'sParadox <-> OmniscientFunctionalChoice. Proof. - auto decomp using + intuition auto using omniscient_fun_choice_imp_small_drinker, omniscient_fun_choice_imp_fun_choice, fun_choice_and_small_drinker_imp_omniscient_fun_choice. @@ -547,7 +547,7 @@ Theorem constructive_indefinite_description_and_small_drinker_iff_epsilon : (EpsilonStatement -> SmallDrinker'sParadox * ConstructiveIndefiniteDescription). Proof. - auto decomp using + intuition auto using epsilon_imp_constructive_indefinite_description, constructive_indefinite_description_and_small_drinker_imp_epsilon, epsilon_imp_small_drinker. @@ -689,7 +689,7 @@ Qed. Corollary dep_iff_non_dep_functional_rel_reification : FunctionalRelReification <-> DependentFunctionalRelReification. Proof. - auto decomp using + intuition auto using non_dep_dep_functional_rel_reification, dep_non_dep_functional_rel_reification. Qed. @@ -814,9 +814,9 @@ Corollary fun_reification_descr_computational_excluded_middle_in_prop_context : (forall P:Prop, P \/ ~ P) -> forall C:Prop, ((forall P:Prop, {P} + {~ P}) -> C) -> C. Proof. - intros FunReify EM C; auto decomp using - constructive_definite_descr_excluded_middle, - (relative_non_contradiction_of_definite_descr (C:=C)). + intros FunReify EM C H. + apply relative_non_contradiction_of_definite_descr; trivial. + auto using constructive_definite_descr_excluded_middle. Qed. (**********************************************************************) |