correctness proof of partial evaluation
this file is a duplication of [PE-STLC-wft-basic-correctness.agda]