proposition: Lemma PFix_F_inv : forall (x:T)(H:D x) (r s:Acc lt x), Acc_iter_partial P F H r = Acc_iter_partial P F H s .
proof: Proof. intro x. intro H. generalize H. pattern x. apply partial_fun_induction. intros. rewrite <- (PFix_F_eq H2 r). rewrite <- (PFix_F_eq H2 s). apply F_ext. auto. auto. Qed.
imports: Ensembles Relations