proposition: Lemma rtc_ind_r_weak (P : A → A → Prop) (Prefl : ∀ x, P x x) (Pstep : ∀ x y z, rtc R x y → R y z → P x y → P x z) : ∀ x z, rtc R x z → P x z.
proof: Proof. cut (∀ y z, rtc R y z → ∀ x, rtc R x y → P x y → P x z). { eauto using rtc_refl. } induction 1; eauto using rtc_r. Qed.
imports: stdpp(options)