module rtc.

type rtc (A -> A -> o) -> (A -> A -> o).

rtc P X X.
rtc P X Z :- (P X Y), (rtc P Y Z).