diff --git a/theories/input_lang_delim/interp.v b/theories/input_lang_delim/interp.v index 6d358f4..a218431 100644 --- a/theories/input_lang_delim/interp.v +++ b/theories/input_lang_delim/interp.v @@ -507,7 +507,7 @@ Section interp. #[export] Instance interp_reset_ne : NonExpansive (interp_reset). Proof. - intros n ???. rewrite /interp_reset. simpl. repeat f_equiv. + intros n ???. rewrite /interp_reset. simpl. repeat f_equiv. by do 2 (intro; simpl; repeat f_equiv). Qed.