proposition: Lemma inj_sval A P : injective (@sval A P).
proof: Proof. move=>[x Hx][y Hy] /= H; move: Hx Hy; rewrite H=>*. congr exist; apply: proof_irrelevance. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq) Eqdep ClassicalFacts