Goal:
  
  ============================
   (FinitelyListable Empty_set)


DEBUG:Going to execute:
split;
            [ cbv[list_all find_index];
               repeat (let t := fresh in
                       intro t; case t; clear t); unshelve
               (repeat
                 match goal with
                 | |- nth_error (?x :: _) 0 = ?rhs => change (Some x = rhs)
                 | |- nth_error (_ :: ?xs) (S ?n) = ?rhs =>
                       change (nth_error xs n = rhs)
                 | |- nth_error ?ev _ = ?rhs =>
                       is_evar ev;
                        (let __ := open_constr:((eq_refl : ev = _ :: _)) in
                         idtac)
                 | |- Some _ = Some _ => reflexivity
                 end); try exact []
            | try instantiate ( 1 := [] ); vm_compute; reflexivity ]