Stream: math-comp users

Topic: ✔ Goal with `\in` and seq


view this post on Zulip Julin Shaji (Mar 22 2024 at 07:40):

Never mind. Got unfold_in with Search.

Goal forall A:Type,
  [::]
    \in (fun w0 : seq A => match w0 with
                           | [::] => true
                           | _ :: _ => false
                           end).
Proof.
  move => A.
  by rewrite unfold_in.
Qed.

view this post on Zulip Notification Bot (Mar 22 2024 at 07:40):

Julin Shaji has marked this topic as resolved.

view this post on Zulip Cyril Cohen (Mar 22 2024 at 08:38):

by [] works.

view this post on Zulip Julin Shaji (Mar 22 2024 at 09:30):

Oh.. :sweat_smile:

view this post on Zulip Julin Shaji (Mar 22 2024 at 09:30):

Now I feel foolish for having spent too much time dwelling on this.


Last updated: Jul 25 2024 at 15:02 UTC