[needs Coq 8.16] add test against f_equiv nonsense
The following proof script actually succeeds currently with Coq 8.15:
Section f_equiv.
Lemma f_equiv1 (fn : nat → gset nat) (x1 x2 : nat) :
fn x1 ⊆ fn x2.
Proof.
(* This used to turn the goal into [x1 ⊆ x2], which is utter nonsense. *)
f_equiv.
This seems like nonsense, and the f_equiv
fails as expected with Coq 8.16. We should add this as a test once we depend on Coq 8.16.
Edited by Ralf Jung