proposition: Lemma in_omap_iff X Y (f : X -> option Y) l y : y el omap f l <-> exists x, x el l /\ f x = Some y.
proof: Proof. induction l; cbn. - firstorder. - destruct (f a) eqn:E; firstorder (subst; firstorder congruence). Qed.
imports: List Lia Undecidability.PCP.PCP