proposition: Lemma doubleton_singleton : forall x, doubleton x x = singleton x.
proof: Proof. ir. ap extensionality; uhg; ir. cp (doubleton_or H). nin H0. rw H0; ap singleton_inc. rw H0; ap singleton_inc. cp (singleton_eq H). rw H0. ap doubleton_first. Qed.
imports: tactics