Goal:
    A : Type  B : A → Type  f : ∀ x : A, B x
  ============================
   (∀ l : list A, make_All_graph l (make_All l))


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