14/11/2020 (Things I learned)
- the details of basic propositional logic, gamified iset.mm with a piton script
- Metamath ACTUALLY relies on meta unformalised "soundness" proofs to know that
  definitions are eliminable and conservative.
- iset.mm is MUCH smaller than set.mm
- Metamath proofs are super hard to shorten
- youtube tries to stalk you through your IP if you try to avoid them?? WTF
- pigeons still get fed after being able to walk and play and spread their wings
- silence (no building construction music) feels great
- sambal ikan keli can scare the lausai demon away