Re: [isabelle] THE - equality



What is the type of x? Did you try x::nat?

2014-04-18 12:24 GMT+02:00 Roger H. <s57076 at hotmail.com>:
> Hello,
>
> how can i prove
>
> (THE x. x + 1 = 3) = 2  ?
>
> After
>
> "apply (rule the_equality, simp)"
>
> i get:
>
> ⋀x. x + 1 = 3 ⟹ x = 2
>
> I think i have to prove that the solution is unique.
> how do i continue?
>
> Thank you!
>




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