proposition: Lemma rest_trans : forall A (P : A -> Prop) (R : relation A), (forall a b, P a -> R b a -> P b) -> forall a, P a -> forall b, trans_clos (rest P R) b a <-> trans_clos R b a.
proof: Proof. intros A P R Inv a Pa b; split. apply trans_incl; intros x y [H _]; assumption. intro H; rewrite trans_clos_trans_clos_alt in H; rewrite trans_clos_trans_clos_alt. induction H as [x y K | x y z K1 K2]. left; repeat split; trivial. apply Inv with y; assumption. assert (Py := Inv _ _ Pa H). right with y. exact (K2 Py). repeat split; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)