Stream: Coq users

Topic: ✔ Implicit coercions for length-indexed list

view this post on Zulip Sebastian Ertel (May 16 2023 at 18:49):

@Paolo Giarrusso , destruct gave me the same error message.

But move => x; rewrite (UIP_refl_nat _ (Nat.add_1_r 0)) //=. really does finish the goal.
Thanks a lot for this hint, @Paolo Giarrusso and @Guillaume Melquiond .

view this post on Zulip Notification Bot (May 16 2023 at 18:50):

Sebastian Ertel has marked this topic as resolved.

Last updated: Oct 04 2023 at 22:01 UTC