proposition: Lemma is_singleton_int a b c: inc c a -> inc c b -> (forall u, inc u a-> inc u b -> u = c) -> singletonp (a \cap b).
proof: Proof. move=> ca cb h;exists c; apply: set1_pr; first by fprops. by move => t /setI2_P [pa pb]; apply : h. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)