proposition: Lemma trans_dec_setI x: alls x trans_dec_set -> trans_dec_set (intersection x).
proof: Proof. case: (emptyset_dichot x). by move => -> _; rewrite setI_0; split => t /in_set0. move=> nea alt; split. move=> a au t ta; apply: (setI_i nea) => y yx. exact: ((proj1 (alt _ yx)) _ (setI_hi au yx)). move: nea=> [y yx] a au; exact: (proj2 (alt _ yx) _ (setI_hi au yx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)