# [isabelle] THE elimination?

```Hi
```
I need to use definite descriptions and can introduce THE using the_equality. But I have found no way to eliminate THE
```
When stuck  at sorry I am faced with
using this:
(THE re. (nam, re) : Ops adt) = rel

goal (1 subgoal):
1. (nam, rel) : Ops adt

My intuitions tell me that this should be obvious but nothing works.
What Have I missed?

david

```
lemma "\<forall> nam rel. ((OpsF nam) =rel) = ((nam, rel)\<in> (adtt.Ops adt))" proof (rule allI)+ fix nam rel show "(OpsF nam = rel) = ((nam, rel) \<in> Ops adt)"
```  unfolding  OpsF_def
proof
assume as: "(THE re. (nam, re) \<in> Ops adt) = rel"  from as
```
show "(nam, rel) \<in> Ops adt" sorry
```
next
```
assume sa: "(nam, rel) \<in> Ops adt" from sa ropsfun [where a=nam and relx=rel] have "\<And> rely. (nam, rely) \<in> Ops adt \<Longrightarrow> rely = rel" by simp with sa show "(THE rel. (nam, rel) \<in> Ops adt) = rel" apply (rule the_equality [where a=rel and P="\<lambda> rel.(nam, rel) \<in> Ops adt "])
```   by auto
qed
qed

```

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