diff options
Diffstat (limited to 'theories/Logic/ClassicalEpsilon.v')
| -rw-r--r-- | theories/Logic/ClassicalEpsilon.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index 0d65a89ba..cee55dc81 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -74,7 +75,7 @@ Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : (** A proof that if [P] is inhabited, [epsilon a P] does not depend on the actual proof that the domain of [P] is inhabited - (proof idea kindly provided by Pierre Castéran) *) + (proof idea kindly provided by Pierre Castéran) *) Lemma epsilon_inh_irrelevance : forall (A:Type) (i j : inhabited A) (P:A->Prop), |