proposition: Lemma lift_perm_lift i j s k' : lift_perm i j s (lift i k') = lift j (s k') :> 'I_n.+1.
proof: Proof. by rewrite permE /lift_perm_fun liftK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)