I have non empty natural number list l1. My requirement is first two elements of this list , therefore i have performed induction twice .(H2 : k1 :: k2 :: t <> [])

Now this list is the input argument to a function g(whose patteren matching is on this list). When i simplify g function it talks about t. How to write that my requirement is k1 ,k2 only ,consider t as nil? I want to test all functions on k1 &k2 only.

if you want to prove that a statement `P`

is true for all lists with 2 elements, you prove `forall l, length l = 2 -> P l`

.

Last updated: Jun 20 2024 at 13:02 UTC