Goal:
    A : Type  R : relation A  S : relation A
  ============================
   (Symmetric R -> Symmetric S -> Symmetric (relation_disjunction R S))


DEBUG:Going to execute:
intros HR HS x y [X| X]; [ left | right ]