[guerrilla]

Lambda calculus is arguably far more abstract because often type theories imply a lot of implrmentation constraints, which makes sense since that's kind of the piount.