# Re: [isabelle] On the use of the rule HOL.refl(exive)

On 27.09.2011 15:29, Alfio Martini wrote:

Dear Isabelle Users,
In the script bellow, I was expecting to solve lemmas 01 and 04 directly by
reflexivity of equality, like the
other ones, since both terms are the same.

`No, the two subtterms left and right of the equality sign are not
``exactly the same. Unfortunately, it is a bit misleading how this goal is
``presented by Isabelle. If you enable the display of types, you get at
``least a hint about what is going wrong:
`
lemma "len Empty = len Empty"
using [[show_types]]
outputs
proof (prove): step 0
goal (1 subgoal):
1. len Empty = len Empty
type variables:
'a, 'b :: type

`As you see, there are two type variables occuring in this term: Empty is
``polymorphic, but there are no constraints, which would enforce a
``particular instantiation of the polymorphic type variable -- not even
``that the types of the left and right Empty should be the same.
`
For this reason, refl is not applicable here.
-- Lars

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