proposition: Lemma lift_inj n (h : 'I_n) : injective (lift h).
proof: Proof. by move=> i1 i2 [/(can_inj (bumpK h))/val_inj]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)