Stream: Coq users

Topic: theorem statement

view this post on Zulip zohaze (Dec 09 2022 at 03:54):

b:nat l:list nat l=[a,a1,a2,a3-----]
I am checking f(b a)=true then f(a a1)=true then
f(a1 a2=true then
f(a2 a3)=true.......
I want to write a lemma,that f ( n1 n2)=true only when it is true for all values of l (or forall a) .Plz help me in writing it in smart way.

Last updated: Jan 27 2023 at 02:04 UTC