Went to Olive Garden with mom, other sister, grandpa, Esther. Tasty chicken parm as always.
Back at home got some work done. I think I actually proved a useful result for the first time in a while, a sort of transitivity property for strict occurrences that has some encouraging implications for the simplicity of this type-reconstruction algorithm. Good chance it's either wrong or old news, but I still feel happy chugging through good ol' N-zillion-case inductions again.
