diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-30 13:10:48 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-30 13:10:48 +0200 |
| commit | fdd5a8452bd2da22ffd1cab3b1888f2261f193b9 (patch) | |
| tree | f343f448f683430a6fc00f9e246745047279e1c3 /theories/Init/Logic.v | |
| parent | 991b78fd9627ee76f1a1a39b8460bf361c6af53d (diff) | |
Functional choice <-> [inhabited] and [forall] commute
Diffstat (limited to 'theories/Init/Logic.v')
| -rw-r--r-- | theories/Init/Logic.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 9ae9dde28..3eefe9a84 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -609,6 +609,11 @@ Proof. destruct 1; auto. Qed. +Lemma inhabited_covariant (A B : Type) : (A -> B) -> inhabited A -> inhabited B. +Proof. + intros f [x];exact (inhabits (f x)). +Qed. + (** Declaration of stepl and stepr for eq and iff *) Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y. |