proposition: Lemma starCA p1 p2 p3 : p1 # p2 # p3 <~> p2 # p1 # p3.
proof: Proof. move=>h; split; case=>h1 [_][->][H1][h2][h3][->][H2] H3 /=; by rewrite unCA; do !esplit. Qed.
imports: mathcomp(ssreflect ssrfun) LemmaOverloading(rels heaps)