## Stream: general

### Topic: inter_subset_union

#### Johan Commelin (Feb 05 2020 at 19:25):

Am I stupid, or are we missing s \cap t \sub s \cup t in the library?

#### Kevin Buzzard (Feb 05 2020 at 19:31):

I know two proofs of that, maybe they couldn't decide which one to use

#### Kevin Buzzard (Feb 05 2020 at 19:31):

Do we have P and Q implies P or Q?

#### Jesse Michael Han (Feb 05 2020 at 19:53):

due to some auspicious [ematch] lemmas in the lattice library, the version for lattices is by {[smt] eblast}

but indeed, library_search fails for the lattice version also.

#### Yury G. Kudryashov (Feb 05 2020 at 20:05):

BTW, where can I read about ematch?

Last updated: May 08 2021 at 18:17 UTC