Goal:
    A : Type  R : relation A
  ============================
   (Symmetric (clos_sym R))


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