Lean Kernel Arena / tutorial/107_proofIrrelevanceUnderBinder

Proof irrelevance applies to any two terms of a proposition, not just to variables. Checking this definition needs aPropFamily (h anElem) ≡ aPropFamily (h anotherElem), i.e. h anElem ≡ h anotherElem. Both are proofs of aProp, since h : aType → aProp, so they are definitionally equal even though their arguments are not. A checker that compares the two applications structurally, without first noticing that they are proofs, wrongly rejects this.