https://ammkrn.github.io/type_checking_in_lean4/trust/trust....