proposition: Lemma set_I2K A B: (A \cap B) \cup A = A.
proof: Proof. apply: extensionality; last by apply:subsetU2r. apply/subU2_setP;split; [ apply:subsetI2l | fprops]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)