Definition value (x1 x2 x3 : nat):= [3;4;5].
Definition content (l :list nat):= value
Definition f4 (a b c : nat)(l:list nat) := f3 a b c content
f3 & f4 are two functions, whose requirement is 4 input arguments (3 nat & list nat) and output bool.
1) I want to write a statement about the existence of f4.
2) No of elements having nat value get change in the list ,how to make it generalize?
Last updated: Oct 13 2024 at 01:02 UTC