diff options
Diffstat (limited to 'theories/Logic/ClassicalDescription.v')
| -rw-r--r-- | theories/Logic/ClassicalDescription.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index a20036f0a5..d76d896585 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -45,7 +45,7 @@ Qed. Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False. Proof. intro HnotEM. -pose (R := fun A b => A /\ true = b \/ ~ A /\ false = b). +set (R := fun A b => A /\ true = b \/ ~ A /\ false = b). assert (H : exists f : Prop -> bool, (forall A:Prop, R A (f A))). apply description. intro A. @@ -75,4 +75,4 @@ destruct (f P). discriminate. assumption. Qed. -
\ No newline at end of file + |