proposition: Lemma serial_Op s1 s2 : Op s1 s2 = s1 ++ s2 :> seq _.
proof: Proof. rewrite /serial; set loop := (X in X [::]); rewrite -/loop. elim: s1 (loop [::] s2) => [n|s11 IHs1 s12 IHs2] //= l. by rewrite IHs1 [in RHS]IHs1 IHs2 catA. Qed.
imports: HB(structures) BinPos BinNat mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq bigop)