Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculusby Michael Rawson09 Jul