Let A, B, f and g be given.
Assume Hdf: graph_domain_subset f A.
Assume Hdg: graph_domain_subset g B.
Let x and y be given.
Assume Hxy: (x,y) ∈ (f ∪ g).
We will prove x ∈ (A ∪ B).
Apply (binunionE f g (x,y) Hxy) to the current goal.
Assume Hxyf: (x,y) ∈ f.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (Hdf x y Hxyf).
An exact proof term for the current goal is (binunionI1 A B x HxA).
Assume Hxyg: (x,y) ∈ g.
We prove the intermediate claim HxB: x ∈ B.
An exact proof term for the current goal is (Hdg x y Hxyg).
An exact proof term for the current goal is (binunionI2 A B x HxB).
∎