proposition: Lemma lub_of_consistent_set : forall A B {I:Inhab B} (E:binary B) (F:(A->B)->(A->B)) (S:(A-->B)->Prop), equiv E -> consistent_set E S -> (forall fi, S fi -> partial_fixed_point E F fi) -> exists (f:A-->B), lub (extends E) S f /\ partial_fixed_point E F f.
proof: Proof. Proof using. introv I Equiv Cons Fixi. sets covers: (fun (x:A) (fi:A-->B) => S fi /\ (dom fi) x). sets D: (fun x => exists fi, covers x fi). sets f: (fun x => if classicT (D x) then epsilon (covers x) x else arbitrary). exists (Build_partial f D). split. split. { intros f' Sf'. split; simpl. intros x Dx. exists~ f'. intros x D'x. unfold f. destruct_if as Dx. epsilon fi. exists~ f'. intros [Si Domi]. apply~ Cons. } { intros f' Upper'. split; simpl. intros x (fi&Ci&Di). apply~ (Upper' fi Ci). intros x Dx. unfold f. destruct_if. epsilon~ fi. intros [Si Domi]. apply~ (Upper' fi). } { intros f' Eq'. simpls. intros x Dx. lets (fi&Ci&Di): Dx. apply~ (Fixi _ Ci). intros y Diy. asserts~ Dy: (D y). apply~ (trans_inv (f y)). unfold f. destruct_if. epsilon~ fj. intros [Sj Domj]. apply~ Cons. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)