proposition: Lemma PFix_eq : forall (x:T )(H:D x), PFix H = F (fun (y:T) (h: lt y x) => PFix (lt_D h)) H.
proof: Proof. intro x; unfold PFix in |- *. intro;rewrite <- (PFix_F_eq (x:=x)). apply F_ext; intros. apply PFix_F_inv. Qed.
imports: Ensembles Relations