finished RecordSub.v
finished Norm.v (normalisation of the simply typed lambda calculus)