Add some sort of rule for `own ∧ own`
The leaf paper has this:
(Coq formalization here.)
Amin suggested something similar a long time ago.
Not sure which formulation works best, but we should have something like that. :)
Whatever the rule is, it should be strong enough to prove things like
Lemma pointsto_and_sep (l1 l2:loc) (v1 v2:val) :
l1 ≠ l2 ->
l1 ↦ v1 ∧ l2 ↦ v2 -∗
l1 ↦ v1 ∗ l2 ↦ v2.
Lemma pointsto_and_eq l x y :
l ↦ x ∧ l ↦ y -∗ ⌜x = y⌝