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


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