proposition: Corollary chain_irrefl n x :~ chain R (S n) x x.
proof: Proof. Proof using Rirrefl Rtrans. intros H. apply chain_trans in H as [ (? & _) | H ]; try easy. revert H; apply Rirrefl. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW.Utils(php) Undecidability.Shared.Libs.DLW.Wf(wf_chains)