proposition: Lemma transitive_extensional x: transitive_set x -> extensional_set x.
proof: Proof. move => tx a b ax bx H; set_extens t => ts. have /setI2_P [] //:inc t (b \cap x). rewrite - H; apply/setI2_P; split => //; apply: (tx _ ax _ ts). have /setI2_P [] //:inc t (a \cap x). rewrite H; apply/setI2_P; split => //; apply: (tx _ bx _ ts). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)