Re: [isabelle] using identity for simplification with different type



On 15.07.2015 18:38, noam neer wrote:
> hi all,
> 
> in the following theory lemma tl1 proves an identity which lemma tl2 tries
> to use.
> however the proof of tl2 fails (tl1's proof works fine.)
> I think the problem is that in tl1 the identity is between reals,
> while in tl2 it is between nats.
> am I correct, and is there a convenient way to use tl1 despite that?

Yes, you are correct and no, there is no convenient way.




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