From c07f1f8d89dd1f975e06e8c45df2c7a4e6ca7fc3 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 27 Feb 2019 17:31:35 +0100
Subject: Add extra eta lemmas for the under tactic

Related: coq/coq#9651
---
 mathcomp/ssreflect/tuple.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/tuple.v')

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.
-- 
cgit v1.2.3