Stream: Coq users

Topic: existence

view this post on Zulip pianke (Feb 04 2023 at 18:11):

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