[isabelle] equality of functions


the lemma "[1 ↦ [4], 2 ↦ [5]] =  [2 ↦ [5], 1 ↦ [4]]" can be proven by auto,

but is there any automatic proof, meaning some existing lemma, which i can add to the simplifier,
so that such identities that occur in the middle of proofs are solved automatically?

Thank you!

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.