proposition: Lemma tack_on_inc: forall x y z:E, (inc z (tack_on x y) ) = (inc z x \/ z = y).
proof: Proof. ir. ap iff_eq. ir; ap tack_on_or. am. ir. nin H. uf tack_on. ap union2_first. am. uf tack_on. ap union2_second. rw H. ap singleton_inc. Qed.
imports: tactics