Remove wfe. Use wf. In Dafny model.