proposition: Fact undiscernable_trans x y z : x ≡ y -> y ≡ z -> x ≡ z.
proof: Proof. unfold undiscernable; eauto. Qed.
imports: List Bool Undecidability.Shared.Libs.DLW.Utils(utils_list finite fin_quotient fin_dec utils_decidable) Undecidability.FOL.TRAKHTENBROT(notations utils decidable)