proposition: Lemma fresh_bijE' (T : finType) (E : {fset nat}) (f : bij T E) x (Hx : x \notin E) : (forall x, fresh_bij' f Hx (inl x) = Sub (val (f x)) (fset1Ur (valP (f x))))* (fresh_bij' f Hx (inr tt) = Sub x fset1U1).
proof: Proof. done. Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries) GraphTheory(bij)