[isabelle] THE - equality



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.