assumption
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
f : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
⊢ ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
no goals