proposition: Lemma allrel_in_l (r : T -> S -> bool) (xs xs' : seq T) (ys : seq S) : xs =i xs' -> allrel r xs ys = allrel r xs' ys.
proof: Proof. by move=>H; rewrite !allrel_allpairsE; apply/eq_all_r/mem_allpairs_dep. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)