proposition: Lemma eq_Rank i i' (j : 'I_(p_ i)) (j': 'I_(p_ i')) : (Rank j == Rank j' :> nat) = (i == i') && (j == j' :> nat).
proof: Proof. rewrite val_eqE /Rank -(can_eq sigK) !rankK. case: (i =P i') => ii' /=; last by case: eqVneq => // -[]. by case: _ / ii' in j' *; rewrite eq_Tagged. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)