proposition: Lemma pad_seqL_leading_true_inj : forall n i j, size i <= n -> size j <= n -> pad_seqL false (true :: i) n.+1 = pad_seqL false (true :: j) n.+1 -> i = j.
proof: Proof. elim=> [[] // [] // | ] n IH i j Hi Hj; rewrite /pad_seqL /= !ltnS !subSS => X. rewrite Hi Hj in X. move: Hi; rewrite leq_eqVlt. case/orP => [/eqP Hi|Hi]. rewrite Hi subnn /= in X. move: Hj; rewrite leq_eqVlt. case/orP => [/eqP Hj|Hj]. by move: X; rewrite Hj subnn /= => -[]. rewrite subSn //= in X; by rewrite -ltnS. move: Hj; rewrite leq_eqVlt. case/orP => [/eqP Hj|Hj]. rewrite Hj subnn /= in X. rewrite subSn //= in X; by rewrite -ltnS. move: X; rewrite !subSn //= => -[] X. apply IH => //. by rewrite /pad_seqL /= Hi Hj !subSS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext