Let f, g and Y be given.
Assume Hrf: graph_range_subset f Y.
Assume Hrg: graph_range_subset g Y.
Let x and y be given.
Assume Hxy: (x,y) ∈ (f ∪ g).
Apply (binunionE f g (x,y) Hxy) to the current goal.
Assume Hxyf: (x,y) ∈ f.
An exact proof term for the current goal is (Hrf x y Hxyf).
Assume Hxyg: (x,y) ∈ g.
An exact proof term for the current goal is (Hrg x y Hxyg).
∎