This is well known. Type theories also do not assume the law of excluded middle. What's your point and it's relevance to the comment?