Goal with `\in` and seq · math-comp users

Stream: math-comp users

Topic: Goal with `\in` and seq

Julin Shaji (Mar 22 2024 at 06:40):

How can this goal be solved?

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

Could we transform this to:

(fun w0 : seq A => match w0 with
   | [::] => true
   | _ :: _ => false
   end) [::] = true.

Last updated: Oct 13 2024 at 01:02 UTC