proposition: Lemma partial_fixed_point_definitions : partial_fixed_point = partial_fixed_point'.
proof: Proof. Proof using. extens. intros A B E F f. unfold partial_fixed_point, partial_fixed_point'. destruct f as [f D]. simpl. iff H. intros [f' P'] [Eff' Pff']. simpls. subst. hnf. simpl. splits~. intros f' Eff'. simpls. forwards H1 H2: (H (Build_partial f' D)). hnf. simpl. splits~. apply H2. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)