proposition: Lemma eqseqP : Equality.axiom eqseq.
proof: Proof. move; elim=> [|x1 s1 IHs] [|x2 s2]; do [by constructor | simpl]. have [<-|neqx] := x1 =P x2; last by right; case. by apply: (iffP (IHs s2)) => [<-|[]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)