I am confused about the evidence and Prop etc. in Coq. How do we prove that (n = n) = (m = m)?
My intention is to show this is somehow True=True. But this is even correct formulation?
What I tried so far is:
Theorem test: forall m n:nat, (n = n) = (m = m).
Proof. intros. simpl.
But simpl. does nothing, and reflexivity neither. This is just an example, in general, I need to prove this for any type X if possible.
n = n and m = m are both propsitions, so they're of sort Prop rather than sort Set. This basically means that n = n is like a statement (that has to be proved) rather than something like true : boolean.
Instead, you could try proving something like: n-n = m-m, or, you could define a function nat_equal : nat -> bool that, given a natural, mapped it to bool, and then prove nat_equal n = nat_equal m.
If you really want to assert that the statements are equal, you'll need propositional extensionality.