Re: [isabelle] On the use of the rule HOL.refl(exive)
The two terms are not identical. Each instance of Empty in len Empty has a separate type.
On 27 Sep 2011, at 14:29, Alfio Martini wrote:
> 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.. But the simplifier tells me
> that I have to use also the equation len01, to substitute len(Empty) for Z.
> What (basic fact) am I missing here?
This archive was generated by a fusion of
Pipermail (Mailman edition) and