diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Z/Interpretations/Relations.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Z/Interpretations/Relations.v b/src/Reflection/Z/Interpretations/Relations.v index 4f33f48bb..963834a10 100644 --- a/src/Reflection/Z/Interpretations/Relations.v +++ b/src/Reflection/Z/Interpretations/Relations.v @@ -579,7 +579,7 @@ Proof. | progress (unfold proj_eq_rel in *; subst) | apply @related_tuples_None_left; constructor | apply -> @related_tuples_Some_left - | apply <- @related_tuples_proj_eq_rel_untuple + | refine (proj2 (@related_tuples_proj_eq_rel_untuple _ _ _ _ _ _) _) | apply <- @related_tuples_lift_relation2_untuple' | progress rewrite ?HList.map'_mapt', <- ?HList.map_is_mapt' | progress rewrite ?Tuple.map_map2, ?Tuple.map2_fst, ?Tuple.map2_snd, ?Tuple.map_id |