I love your posts! The Social Filesystem is amazing!

https://overreacted.io/a-social-filesystem/

        induction b with d hd
        rw [add_zero, zero_add]
        rfl
        rw [add_succ, succ_add]
        rw [hd]
        rfl

i really enjoyed finally internalizing dependent type theory. it helped a lot with that.