proposition: Lemma transitive_setU x: alls x transitive_set -> transitive_set (union x).
proof: Proof. move=> alt a /setU_hi [y ay yx] t ta. move: (((alt _ yx) _ ay) _ ta) => ty; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)