01/12/2020 (things i learned)
- Proved `nat.fact` is primitive recursive in Lean!
- Know what CIC (calculus of inductive constructions) and
  Strong Normalization Property means
- revise mathlib's implementation of primrec
- Grokxzlkjzy's (not actual name so not counted) heirarchy
  basically just +, x, ^, tetration, .... (super cool)
- .elan runs away from my $PATH every time i log in hmmm