Goal:
    A : Type  R : relation A  S : relation A
  ============================
   (inclusion R (relation_disjunction R S))


DEBUG:Going to execute:
intros x y H; left
DEBUG LTAC Evaluated term: clos_rt_monotone