proposition: Lemma bij_castE x (Hx : x \in A) : bij_cast [` Hx] = [` cast_proof Hx].
proof: Proof. rewrite /bij_cast. move: (cast_proof _). case eqA => Hx'. exact: val_inj. Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries) GraphTheory(bij)