• How to prove that two sets are different?
• Is there an axiom-free proof of Streicher's axiom K for the equality on nat?
• How to prove that two proofs of n <= m on nat are equal?
• How to exploit equalities on sets?
• I have a problem of dependent elimination on proofs, how to solve it?
• And what if I want to prove the following?