proposition: Lemma join_lookup_Some_same_length' n ls j i x : Forall (λ l, length l = n) ls → i < n → mjoin ls !! (j * n + i) = Some x ↔ ∃ l, ls !! j = Some l ∧ l !! i = Some x.
proof: Proof. intros. rewrite join_lookup_Some_same_length by done. split; [|naive_solver]. destruct 1 as (j'&l'&i'&?&?&Hj); decompose_Forall. assert (i' < length l') by eauto using lookup_lt_Some. apply Nat.mul_split_l in Hj; naive_solver. Qed.
imports: stdpp(options)