let destruct a =
  assert(is_app a);
  match a with App(f,l) -> (f,l) | _ -> assert false