proposition: Lemma Fix_prop_eq_unique_fixed_point : forall (A:Type) (E:binary A) (F:A->A) (x:A), Fix_prop E E F x = unique_fixed_point E F x.
proof: Proof. Proof using. intros. extens. iff [Fx Ux]. split; intros y Hy. apply~ Fx. apply~ Ux. split; intros y Hy. apply~ Fx. apply~ Ux. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)