proposition: Lemma repS mx n : rep n.+1 mx = rep n mx >> mx.
proof: Proof. elim: n => /= [|n IH]; first by rewrite bindmskip bindskipf. by rewrite bindA IH. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy