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: Oct 04 2023 at 21:01 UTC