diff options
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/Tuple.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index de1af2a95..6802a86c3 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -66,8 +66,9 @@ Defined. Global Instance Equivalence_fieldwise' {A} {R:relation A} {R_equiv:Equivalence R} {n:nat}: Equivalence (fieldwise' n R). Proof. - induction n; [solve [auto]|]. - simpl; constructor; repeat intro; intuition eauto. + induction n as [|? IHn]; [solve [auto]|]. + (* could use [dintuition] in 8.5 only, and remove the [destruct] *) + destruct IHn, R_equiv; simpl; constructor; repeat intro; intuition eauto. Qed. Global Instance Equivalence_fieldwise {A} {R:relation A} {R_equiv:Equivalence R} {n:nat}: @@ -77,4 +78,4 @@ Proof. Qed. Arguments fieldwise' {A B n} _ _ _. -Arguments fieldwise {A B n} _ _ _.
\ No newline at end of file +Arguments fieldwise {A B n} _ _ _. |