proposition: Fact gfp_fix x y : F gfp x y <-> gfp x y.
proof: Proof. Proof using i_decr i_S gfp_fix1 gfp_fix0 HF4 HF0. split; auto. Qed.
imports: List Arith Nat Lia Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite php) Undecidability.FOL.TRAKHTENBROT(notations)