Goal:
    A : Type
  ============================
   (Transitive option_extends)


DEBUG:Going to execute:
intros x y z [] H; inv H