rfl
case mk.refl
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
g : a ⟶ b
isFunction✝ : IsFunction g.1
dom_eq✝ : dom g.1 = a
ran_subset✝ : ran g.1 ⊆ b
h :
  ∀ (x : V),
    x ∈ a →
      apply { graph := g.1, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ }.graph x =
        apply g.graph x
⊢ { graph := g.1, isFunction := isFunction✝, dom_eq := dom_eq✝, ran_subset := ran_subset✝ } = g
no goals