I have natural number list l= [a1;a2;a3...an] and function f. First f takes a1 and generate l1,then f take a2 and generate l2...

I have information that In a2 l1 & In a3 l2....

H=c1=a1 & H2=In c2 l . It means c2 is not equal to a1 but it could be a2 or any element of l. Now want to write a lemma to prove

that c2 could be any element except a1 and hold the property which all oth er elements hold(including c2 and all previous elements like a1 a2..)

why `c2`

is not equal to `a1`

?

I have solved the case where c2=a1 . Now this is the case where (a1=c1) & c2 is not equal to a1 but it could be any other element of the list.

```
c1 = a1 -> In c2 (a2 :: ... :: an) -> P c1 c2
```

Last updated: Oct 04 2023 at 20:01 UTC