l have natural number list l1 then pass it as input argument to function z(l1 l2 l3) (bool output). After applying induction first time l1 becomes l1=[c0::t]. In H1: [c0::t] <>nil->

if eqlist l2 l3 then z(l1 l2 l3)=true else false...

After applying induction second time l1=[c0::c1::t]. then get H2.But this process never ends.I want to ask may i use H1 in H2? What to do? I am applying induction on l1 then empty case get easily resolve but in second case i am testing the conditions on new elements [c0::c1::c2....]

can you give exact coq code?

Last updated: Oct 04 2023 at 20:01 UTC