proposition: Theorem discernable_discriminable_list l : discriminable_list l.
proof: Proof. Proof using H2. apply DEC_PER_list_proj_finite_discrete with (l := l) (R := undiscernable). + split; eauto. + red; apply discernable_dec_undiscernable_dec. + intros; auto. Qed.
imports: List Bool Undecidability.Shared.Libs.DLW.Utils(utils_list finite fin_quotient fin_dec utils_decidable) Undecidability.FOL.TRAKHTENBROT(notations utils decidable)