proposition: Lemma list_lookup_fmap_inv l i x : (f <$> l) !! i = Some x → ∃ y, x = f y ∧ l !! i = Some y.
proof: Proof. intros Hi. rewrite list_lookup_fmap in Hi. destruct (l !! i) eqn:?; simplify_eq/=; eauto. Qed.
imports: stdpp(options)