proposition: Lemma catl2_infix s s1 s2 : infix (s1 ++ s) (s2 ++ s) -> infix s1 s2.
proof: Proof. by rewrite -infix_rev !rev_cat => /catr2_infix; rewrite infix_rev. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)