proposition: Fact chain_trans n x y : chain R n x y -> n = 0 /\ x = y \/ R x y.
proof: Proof. Proof using Rtrans. induction 1 as [ | ? ? ? ? ? ? [ [] | ] ]; subst; eauto. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW.Utils(php) Undecidability.Shared.Libs.DLW.Wf(wf_chains)