Hi, I'm just having a look at the lemmas about disjoint
and
Lemma disjoint_trans A B C : A \subset B -> [disjoint B & C] -> [disjoint A & C].
seems like an odd/poor choice. How about deprecating this name in favor of something like disjointWl
(weaken left) and adding disjointWr
and disjointW
? Alternatively also disjointSl
(subset left).
Last updated: May 31 2023 at 04:01 UTC