proposition: Lemma wf_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) <-> well_founded (rest P R)).
proof: Proof. intros A R P Inv; split. intros W a; rewrite <- acc_rest; trivial. apply W. intros W a; rewrite acc_rest; trivial. Qed.
imports: Coq(Setoid Relations List Wellfounded)