proposition: Lemma set_U2K A B: (A \cup B) \cap A = A.
proof: Proof. apply: extensionality; first by apply:subsetI2r. apply/subsetI2_P;split; [ apply:subsetU2l | fprops]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)