DATX11-VT26-33_NiSm_Haskell_proof.pdf