proposition: Lemma unliftP n (h i : 'I_n) : unlift_spec h i (unlift h i).
proof: Proof. rewrite /unlift; case: insubP => [u nhi | ] def_i /=; constructor. by apply: val_inj; rewrite /= def_i unbumpK. by rewrite negbK in def_i; apply/eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)