[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.