proposition: Lemma rtc_ind_r (P : A → Prop) (x : A) (Prefl : P x) (Pstep : ∀ y z, rtc R x y → R y z → P y → P z) : ∀ z, rtc R x z → P z.
proof: Proof. intros z p. revert x z p Prefl Pstep. refine (rtc_ind_r_weak _ _ _); eauto. Qed.
imports: stdpp(options)