proposition: Lemma join_lookup_Some_same_length n ls i x : Forall (λ l, length l = n) ls → mjoin ls !! i = Some x ↔ ∃ j l i', ls !! j = Some l ∧ l !! i' = Some x ∧ i = j * n + i'.
proof: Proof. intros Hl. rewrite join_lookup_Some. f_equiv; intros j. f_equiv; intros l. f_equiv; intros i'. assert (ls !! j = Some l → j < length ls) by eauto using lookup_lt_Some. rewrite (sum_list_fmap_same n), take_length by auto using Forall_take. naive_solver lia. Qed.
imports: stdpp(options)