proposition: Lemma fcatAC (s1 s2 s3 : fmap) : [&& disj s1 s2, disj s2 s3 & disj s1 s3] -> fcat s1 (fcat s2 s3) = fcat s2 (fcat s1 s3).
proof: Proof. by case/and3P=>H1 H2 H3; rewrite -!fcatA // (@fcatC s1 s2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)