diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index d9d8b7670..699051ec1 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -112,7 +112,7 @@ Exists y. Split. NewDestruct HR''xy' as [H'Px HR'xy']. Rewrite proof_irrel with a1:=HPx a2:=H'Px. Exact HR'xy'. -.Qed. +Qed. Definition IndependenceOfPremises := (A:Type)(P:A->Prop)(Q:Prop)(Q->(EXT x|(P x)))->(EXT x|Q->(P x)). |