There is a theorem in CPDT which is brushed off with a solution using a custom tactic (crush) defined by the author

```
Theorem length_app : ∀ ls1 ls2 : list, length (app ls1 ls2 ) = plus (length ls1) (length ls2).
induction ls1; crush.
Qed.
```

And I'm trying to use built-in tactics to understand this proof and prove this.

I am stuck at a point where I need to prove the following

```
T: Set
t: T
ls2: list
IHls2: length ls2 = plus O (length ls2)
-----------------------------------------------------------------------
(1/1)
S (length ls2) = plus (S O) (length ls2)
```

and I want to be able to remove the church notation S. But I don't know what tactic I should use

If you do `Search plus S`

you can find lemmas about `S`

and `plus`

. There ought to be a lemma about turning `plus (S x) y = S (plus x y)`

Then you can use `rewrite`

along that equality.

or `rewrite <-`

if it needs to go the otherway

There is also a lemma about `plus O x = x`

somewhere but you probably don't need that since `IHls2`

gives you what you want.

The lemma `f_equal`

should help with proving `S x = S y`

from `x = y`

. You can just `apply`

it.

Thanks @Ali Caglayan that worked!

Ali Caglayan has marked this topic as resolved.

Last updated: Sep 23 2023 at 14:01 UTC