diff options
| -rw-r--r-- | src/Spec/PointEncoding.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v index 6c6e3fa9d..99726f311 100644 --- a/src/Spec/PointEncoding.v +++ b/src/Spec/PointEncoding.v @@ -361,7 +361,7 @@ Section PointEncoding. rewrite option_map_option_rect. eapply option_rect_shuffle with (EQD := Keq). + apply Algebra.monoid_Equivalence. - + apply Tuple.Equivalence_fieldwise. + + apply (@Tuple.Equivalence_fieldwise K _ _ 2). + apply Proper_Kcoordinates_from_y; auto. + cbv [Encoding.dec Fencoding]. apply phi_decode. |