proposition: Lemma mem_cast m n (H : m = n) (i : 'I_m) (S : {set 'I_m}) : (cast_ord H i) \in [set cast_ord H i | i in S] = (i \in S).
proof: Proof. exact/mem_imset/cast_ord_inj. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype finfun fintype choice seq tuple) mathcomp(finset tuple bigop) tools