proposition: Lemma set3_P a b c x: inc x (tripleton a b c) <-> [\/ x = a , x = b | x = c].
proof: Proof. split; last by rewrite /tripleton;case => ->; fprops. case /setU1_P; [case /set2_P | ]; in_TP4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)