proposition: Theorem gfp_decidable : dec gfp.
proof: Proof. Proof using i_dup i_decr i_dec i_S gfp_reached gfp_fix1 HF6 HF5 HF0. destruct gfp_finite_t as (n & Hn). intros x y; destruct (i_dec n x y); [ left | right ]; rewrite Hn; tauto. Qed.
imports: List Arith Nat Lia Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite php) Undecidability.FOL.TRAKHTENBROT(notations)