# [isabelle] Question to Sledgehammer output

`I get the following sledgehammer output (using E). It talks about a type
``unification error, what does this mean ?
``The proposed metis command seems to run very long (I aborted it after a
``few minutes and wrote by (induct x) auto in the meantime ;))
`
Subgoal 1:
map snd (map (\<lambda>(a, b). (f a, b)) x) = map snd x
Try this command:

`apply (metis Pair_eq Set.subsetI finite finite_surj finite_surj_inj
``id_apply injD inj_on_id inv_f_f inv_id not_Cons_self rangeI snd_eqD
``surjective_pairing)
`
Translation of TSTP raised an exception: Type unification failed
Type error in application: Incompatible operand type

`Operator: op ` :: (?'X5.0 \<Rightarrow> ?'X6.0) \<Rightarrow> ?'X5.0
``set \<Rightarrow> ?'X6.0 set
`Operand: snd :: ?'X1.0 \<times> ?'X2.0 \<Rightarrow> ?'X2.0
regards,
Peter

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