I'm just going over the sequence of lemmas that I proved about `subseq`

, `index`

, `rot`

, and the likes and which I plan to PR. But I'm still looking for some good lemma names. What would be good names for the following (assuming the statements are in the right form to begin with):

```
Lemma eqseq_??? (T : eqType) (s1 s2 s3 s4 : seq T) (x : T) :
uniq (s3 ++ x :: s4) -> s1 ++ x :: s2 == s3 ++ x :: s4 = (s1 == s3) && (s2 == s4).
Lemma subseq_??? (T : eqType) (s1 s2 s3 s4 : seq T) x :
uniq (s3 ++ x :: s4) -> subseq (s1 ++ x :: s2) (s3 ++ x :: s4) -> subseq s1 s3 /\ subseq s2 s4.
```

Christian Doczkal said:

I'm just going over the sequence of lemmas that I proved about

`subseq`

,`index`

,`rot`

, and the likes and which I plan to PR. But I'm still looking for some good lemma names. What would be good names for the following (assuming the statements are in the right form to begin with):`Lemma eqseq_??? (T : eqType) (s1 s2 s3 s4 : seq T) (x : T) : uniq (s3 ++ x :: s4) -> s1 ++ x :: s2 == s3 ++ x :: s4 = (s1 == s3) && (s2 == s4). Lemma subseq_??? (T : eqType) (s1 s2 s3 s4 : seq T) x : uniq (s3 ++ x :: s4) -> subseq (s1 ++ x :: s2) (s3 ++ x :: s4) -> subseq s1 s3 /\ subseq s2 s4.`

yes indeed, I think we need a name for this pattern `s1 ++ x :: s2`

and decide once and forall whether which of the former and `rcons s1 x ++ s2`

we prefer as a canonical formulation.

Last updated: Feb 09 2023 at 02:02 UTC