fact: Fixpoint iter_joinable (l : list A) (u : A) (j : A) : Prop := match l with | nil => u = j | x :: l' => exists j', iter_joinable l' u j' /\ join x j' j end.
imports: VST.msl.base VST.msl.sepalg VST.msl.sepalg_generators