I'm trying to prove the following lemma:

```
Lemma ctx_pos_dec:
forall {X : Type} (G G' D D': slist X) (A: X) (i : nat),
(G, A);G' = (D, A); D' -> ((G, A);G')!i = Some A -> ((D, A);D')!i = Some A
-> G = D /\ G' = D'.
Proof.
intros.
split.
```

where slists are defined as snoc lists, and the ! operator works as nth in lists counting from right to left, but I'm not able to find something useful in the standard library about nth or list's concatenation. I was thinking about a lemma to show that if ((G, A); G') ! i = Some A and ((D, A); D') ! i = Some A, then G,A = D,A /\ G' = D' and that would be easy I guess, that's a good approach?

I'm doubting about that my helper lemma would be even easy to prove or impossible :thinking:

Is the following an appropriate translation of your statement with usual lists?

```
Lemma ctx_pos_dec:
forall {X : Type} (G G' D D': list X) (A: X) (i : nat),
G' ++ A :: G = D' ++ A :: D -> nth_error (G' ++ A :: G) i = Some A -> nth_error (D' ++ A :: D) i = Some A
-> G = D /\ G' = D'.
```

If so, you probably need some additional hypotheses like "each element occurs at most once in the lists" otherwise the statement is false. Consider `G = D' = [0]`

, `G' = D = []`

, `A = 0`

and `i = 1`

.

Last updated: May 19 2024 at 18:02 UTC