proposition: Lemma set_subset_single_r a s : s ⊆₁ eq a <-> s ≡₁ eq a \/ s ≡₁ ∅.
proof: Proof. u; intuition; firstorder. destruct (classic (exists b, s b)) as [M|M]; desf. left; split; ins; desf; eauto. specialize (H _ M); desf. right; split; ins; eauto. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms