diff options
| author | Cyril Cohen | 2019-03-29 13:07:26 +0100 |
|---|---|---|
| committer | GitHub | 2019-03-29 13:07:26 +0100 |
| commit | 850862dc6475bd48524a294651400df4b5b7ecf3 (patch) | |
| tree | 9a00564e1a51d5bc15ddb7ed7a73c14932f387e9 /mathcomp/ssreflect/tuple.v | |
| parent | 85a3a1ac7f6548a9489fe860d40e5ab110417569 (diff) | |
| parent | c07f1f8d89dd1f975e06e8c45df2c7a4e6ca7fc3 (diff) | |
Merge pull request #292 from erikmd/under-support
Add extra eta lemmas for the under tactic
Diffstat (limited to 'mathcomp/ssreflect/tuple.v')
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index 8f81155..c0ba403 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -411,10 +411,14 @@ Proof. by rewrite -tnth_nth tnth_mktuple. Qed. End MkTuple. +Lemma eq_mktuple T' (f1 f2 : 'I_n -> T') : + f1 =1 f2 -> mktuple f1 = mktuple f2. +Proof. by move=> eq_f; apply eq_from_tnth=> i; rewrite !tnth_map eq_f. Qed. + End UseFinTuple. Notation "[ 'tuple' F | i < n ]" := (mktuple (fun i : 'I_n => F)) (at level 0, i at level 0, format "[ '[hv' 'tuple' F '/' | i < n ] ']'") : form_scope. - +Arguments eq_mktuple {n T'} [f1] f2 eq_f12. |