proposition: Lemma rec_fixed_point_generally_consistent' : forall A B {IB:Inhab B} (F:(A->B)->(A->B)) (R:binary A) (P:A->Prop) (E:binary B) f, equiv E -> wf R -> rec_contractive' E P F R f -> fixed_point (pfun_equiv E P) F f -> generally_consistent_partial_fixed_point E F (Build_partial f P).
proof: Proof. Proof using. introv IB Equiv Wf Cont Fixf. split. unfolds. simpl. apply Fixf. intros [f' P'] Fixf'. sets f'': (fun x => if classicT (P' x) then f' x else f x). intros x [Px P'x]. simpls. cuts Ind: (forall x, P x -> E (f x) (f'' x)). apply~ (trans_inv (f'' x)). unfold f''. destruct_if. apply~ refl_inv. clears x. intros x. induction_wf IH: Wf x. intros Px. destruct (prop_inv (P' x)) as [P'x|NP'x]; [| unfold f''; destruct_if; apply~ refl_inv ]. apply~ (trans_sym_lr (F f'' x)). apply~ (trans_inv (F f x)). apply~ Fixf. apply~ equiv_refl. apply~ (Fixf' (Build_partial f'' P')). simpl. intros y P'y. unfold f''. destruct_if~. apply~ refl_inv. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)