proposition: Lemma join_lookup_Some ls i x : mjoin ls !! i = Some x ↔ ∃ j l i', ls !! j = Some l ∧ l !! i' = Some x ∧ i = sum_list (length <$> take j ls) + i'.
proof: Proof. revert i. induction ls as [|l ls IH]; csimpl; intros i. { setoid_rewrite lookup_nil. naive_solver. } rewrite lookup_app_Some, IH. split. - destruct 1 as [?|(?&?&?&?&?&?&?)]. + eexists 0. naive_solver. + eexists (S _); naive_solver lia. - destruct 1 as [[|?] ?]; naive_solver lia. Qed.
imports: stdpp(options)