# Re: [isabelle] Odd failure to match local statement with pending goal.

```On 28.07.2011 12:45, Lawrence Paulson wrote:
```
```I'm afraid I can't. In general, the name of a bound variable should be irrelevant. I considered the possibility of a hidden effect on type inference, but all variables have the same type, namely tree.

Strange.
```
```
```
Indeed. When I tried to find a minimal example, I found that it goes away, when I try to remove the initial proof steps:
```
-----------------
lemma "⋀x. x ∈ {z. ∃r' s'. r' ∈ closure r ∧ s' ∈ {z. ∃r' s'. r' ∈
closure s ∧ s' ∈ closure t ∧ z = Node r' s'} ∧ z = Node r' s'} ⟹
x ∈ {z. ∃r' s'. r' ∈ {z. ∃r' s'. r' ∈ closure r ∧ s' ∈ closure
s ∧ z = Node r' s'} ∧ s' ∈ closure t ∧ z = Node r' s'}"
apply (unfold mem_Collect_eq)
apply (elim exE conjE)
proof -
fix x r' s' r'a

assume "x = Node r' s'" and "r'a ∈ closure s"
then show "∃r' s'.
(∃r'a s'. r'a ∈ closure r ∧ s' ∈ closure s
∧ r' = Node r'a s') ∧
s' ∈ closure t ∧ x = Node r' s'"
oops
-----------------

```
still exhibits this behabiour, but if I remove the unfold too, it goes away. The show statement in the following snippet works just fine:
```
-----------------
lemma "⋀x. ∃r' s'. r' ∈ closure r ∧ (∃r' s'a. r' ∈ closure s ∧ s'a ∈
closure t ∧ s' = Node r' s'a) ∧ x = Node r' s' ⟹
∃r' s'. (∃r'a s'. r'a ∈ closure r ∧ s' ∈ closure s ∧ r' = Node r'a
s') ∧ s' ∈ closure t ∧ x = Node r' s'"
apply (elim exE conjE)
proof -
fix x r' s' r'a

assume "x = Node r' s'" and "r'a ∈ closure s"
then show "∃r' s'.
(∃r'a s'. r'a ∈ closure r ∧ s' ∈ closure s
∧ r' = Node r'a s') ∧
s' ∈ closure t ∧ x = Node r' s'"
sorry
oops
-----------------

```

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