Goal:
    A : Type  H : ReflectEq A
  ============================
   (∀ l1 l2 : list A, split_prefix_graph l1 l2 (split_prefix l1 l2))


DEBUG:Going to execute:
let eos := fresh "eos" in
           pose proof CoreTactics.the_end_of_the_section as eos