proposition: Lemma inclusion_minus_l s : r \ r' ⊆ s <-> r ⊆ r' ∪ s.
proof: Proof. unfold minus_rel, union, inclusion; split; ins; desf. 2: by eapply H in H0; desf; eauto. by destruct (classic (r' x y)); eauto. Qed.
imports: HahnBase HahnList Relations