diff options
author | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-02-27 14:04:18 +0000 |
---|---|---|
committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-02-27 14:04:18 +0000 |
commit | c3662482d3d9f4bda5f5d0e92f1b2367954b8af3 (patch) | |
tree | 8f481539f6d10911225c5ec3653b3079b8184324 /theories | |
parent | e3124e098ef8170dac2b348b91757a7034bc4999 (diff) |
[stdlib] move “Require” out of sections
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Logic/Diaconescu.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index c124e7141..6a1c88341 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -40,6 +40,7 @@ [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent to AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. *) +Require ClassicalFacts ChoiceFacts. (**********************************************************************) (** * Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *) @@ -54,7 +55,7 @@ Definition PredicateExtensionality := (** From predicate extensionality we get propositional extensionality hence proof-irrelevance *) -Require Import ClassicalFacts. +Import ClassicalFacts. Variable pred_extensionality : PredicateExtensionality. @@ -76,7 +77,7 @@ Qed. (** From proof-irrelevance and relational choice, we get guarded relational choice *) -Require Import ChoiceFacts. +Import ChoiceFacts. Variable rel_choice : RelationalChoice. @@ -89,7 +90,7 @@ Qed. (** The form of choice we need: there is a functional relation which chooses an element in any non empty subset of bool *) -Require Import Bool. +Import Bool. Lemma AC_bool_subset_to_bool : exists R : (bool -> Prop) -> bool -> Prop, @@ -161,6 +162,8 @@ End PredExt_RelChoice_imp_EM. Section ProofIrrel_RelChoice_imp_EqEM. +Import ChoiceFacts. + Variable rel_choice : RelationalChoice. Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y. |