proposition: Fact gfp_greatest R : R ⊆ F R -> R ⊆ gfp.
proof: Proof. Proof using HF0. intros HR x y H n; revert x y H. induction n as [ | n IHn ]. + now auto. + apply incl_trans with (1 := HR). rewrite iS; apply HF0; auto. Qed.
imports: List Arith Nat Lia Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite php) Undecidability.FOL.TRAKHTENBROT(notations)