Archived tweet #5976 from the @leastfixedpoint Twitter Archive

Proof-irrelevance isn't working for me. Somehow I believe the types of the proofs are the same, but Coq doesn't? I must be missing something