Goal:
  
  ============================
   (forall t : Empty_set,
    nth_error (list_all Empty_set) (find_index t) = Some t)


DEBUG:Going to execute:
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)