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: Aug 11 2022 at 03:02 UTC