Stream: Coq users

Topic: bool data type

zohaze (Jun 03 2023 at 18:02):

Lemma is_x: forall  x l,
f1 x l && f l = true->
In x  l.

Without the information of f1 & f ,could i link bool and proposition?

Michael Soegtrop (Jun 05 2023 at 07:37):

No. f1 could be a function which always returns false and f anyway doesn't get x as argument, so it could not possibly tell something about if x is in l.

Last updated: Oct 13 2024 at 01:02 UTC