[drumnerd]

In type checking, particularly in dependent types, it is not trivial to check that two types are the same. Different notions of equality are useful in this field. A type can contain a function value inside. How to prove that two functions are the same? Is not enough to prove that for all X f X and g X implies f is g.

[auggierose]

Don't use types for logic. It will lead to confused statements like yours.