Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn

use_thys ["Paper"];