proposition: Lemma Restricted_acc_eq_acc : forall R a, Acc (fun a a' => P a /\ R a a') a <-> Restricted_acc R a.
proof: Proof. intros R a. split. intro acc_a; induction acc_a as [a acc_a IHa]. constructor; trivial. intros a' Pa' Ha'. apply IHa; split; trivial. intro Raa; induction Raa as [a Raa IHa]. constructor. intros a' Ha'; elim Ha'; clear Ha'; intros Pa' Ra'a. apply (IHa a' Pa' Ra'a). Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil)