proposition: Lemma acc_rest : forall A (R : relation A) (P : A -> Prop), (forall (a b : A), P a -> R b a -> P b) -> (forall a, (P a -> Acc R a) <-> Acc (rest P R) a).
proof: Proof. intros A R P Inv a; split. intro K; apply Acc_intro; intros b [H [Wb Wa]]. apply Acc_inv with a; trivial. apply Acc_incl with R. clear; intros a b [H _]; assumption. apply K; assumption. repeat split; assumption. intro Acc_a; induction Acc_a as [a Acc_a IH]. intro Pa; apply Acc_intro; intros b H. apply IH. repeat split; trivial. apply Inv with a; assumption. apply Inv with a; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)