proposition: Lemma lookup_set_to_map_id `{FinSet (K * A) C} (X : C) i x : (∀ i y y', (i,y) ∈ X → (i,y') ∈ X → y = y') → (set_to_map id X : M A) !! i = Some x ↔ (i,x) ∈ X.
proof: Proof. intros. etrans; [apply lookup_set_to_map|naive_solver]. intros [] [] ???; simplify_eq/=; eauto with f_equal. Qed.
imports: Coq(Permutation) stdpp(options)