Comment by physPop

yes thats the main reason, agda , coq similar ideas