diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-01 10:26:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-01 11:33:55 +0200 |
| commit | 76adb57c72fccb4f3e416bd7f3927f4fff72178b (patch) | |
| tree | f8d72073a2ea62d3e5c274c201ef06532ac57b61 /theories/FSets/FSetBridge.v | |
| parent | be01deca2b8ff22505adaa66f55f005673bf2d85 (diff) | |
Making those proofs which depend on names generated for the arguments
in Prop of constructors of inductive types independent of these names.
Incidentally upgraded/simplified a couple of proofs, mainly in Reals.
This prepares to the next commit about using names based on H for such
hypotheses in Prop.
Diffstat (limited to 'theories/FSets/FSetBridge.v')
| -rw-r--r-- | theories/FSets/FSetBridge.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 6aebcf501..97f140b39 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -673,24 +673,24 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x (filter f s) -> In x s. Proof. - intros s x f; unfold filter; case M.filter; intuition. - generalize (i (compat_P_aux H)); firstorder. + intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition. + generalize (Hiff (compat_P_aux H)); firstorder. Qed. Lemma filter_2 : forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x (filter f s) -> f x = true. Proof. - intros s x f; unfold filter; case M.filter; intuition. - generalize (i (compat_P_aux H)); firstorder. + intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition. + generalize (Hiff (compat_P_aux H)); firstorder. Qed. Lemma filter_3 : forall (s : t) (x : elt) (f : elt -> bool), compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s). Proof. - intros s x f; unfold filter; case M.filter; intuition. - generalize (i (compat_P_aux H)); firstorder. + intros s x f; unfold filter; case M.filter as (x0,Hiff); intuition. + generalize (Hiff (compat_P_aux H)); firstorder. Qed. Definition for_all (f : elt -> bool) (s : t) : bool := |