Definition relation (A : Type) := A -> A -> Prop.

(** The syntax {param} declares the parameter [param] as implicit. In the case
of [rtc], it allows one to write [rtc R x y] instead of [rtc A R x y]. *)

Inductive rtc {A} (R : relation A) : relation A :=
  | rtc_refl x : rtc R x x
  | rtc_l x y z : R x y -> rtc R y z -> rtc R x z.

Definition gen_dp {A} (R T : relation A) := forall x y1 y2,
  R x y1 -> T x y2 -> exists z, T y1 z /\ R y2 z.

Lemma gen_dp_sym {A} (R T : relation A) :
  gen_dp R T -> gen_dp T R.
Proof.
  (* exercise *)
Qed.

Definition dp {A} (R : relation A) := gen_dp R R.
Definition cr {A} (R : relation A) := dp (rtc R).

Lemma rtc_gen_dp {A} (R T : relation A) :
  gen_dp R T -> gen_dp (rtc R) T.
Proof.
  (* exercise *)
Qed.

Lemma dp_cr {A} (R : relation A) :
  dp R -> cr R.
Proof.
  (* exercise *)
Qed.