diff options
Diffstat (limited to 'mathcomp/ssreflect/seq.v')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index fab3fa9..999ec0a 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -2385,9 +2385,9 @@ Notation "[ 'seq' E : R | i : T <- s & C ]" := Lemma filter_mask T a (s : seq T) : filter a s = mask (map a s) s. Proof. by elim: s => //= x s <-; case: (a x). Qed. -Lemma all_sigP T a (s : seq T) : all a s -> {s' : seq (sig a) | map sval s' = s}. +Lemma all_sigP T a (s : seq T) : all a s -> {s' : seq (sig a) | s = map sval s'}. Proof. -elim: s => /= [_|x s ihs /andP [ax /ihs [s' <-]]]; first by exists [::]. +elim: s => /= [_|x s ihs /andP [ax /ihs [s' ->]]]; first by exists [::]. by exists (exist a x ax :: s'). Qed. |