proposition: Lemma PFix_F_eq : forall (x:T)(H:D x)(r:Acc lt x), F (fun (y:T) (h: lt y x) => Acc_iter_partial P F (lt_D h) (Acc_inv r y h))H = Acc_iter_partial P F H r.
proof: Proof. destruct r using Acc_inv_dep. auto. Qed.
imports: Ensembles Relations