proposition: Lemma fix_phi : forall (A:Type)(t:A->option bool) f, F_phi A t f (phi t f) = phi t f.
proof: Proof. intros A t f. assert (Hint : least_fixpoint (f_order' A) (F_phi A t f) (phi t f)). unfold phi, f_order'; apply Tarski_fix_prop; apply F_phi_continuous. unfold least_fixpoint in Hint; fold (phi t f) in Hint. intuition. Qed.
imports: Relations ClassicalEpsilon function_cpo constructs syntax little