yes thats the main reason, agda , coq similar ideas