proposition: Lemma eqseq_rcons s1 s2 x1 x2 : (rcons s1 x1 == rcons s2 x2) = (s1 == s2) && (x1 == x2).
proof: Proof. by rewrite -(can_eq revK) !rev_rcons eqseq_cons andbC (can_eq revK). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)