Let A, B, f and g be given.
Assume Hdisj: A ∩ B = Empty.
Assume Hdomf: graph_domain_subset f A.
Assume Hdomg: graph_domain_subset g B.
Assume Hfunf: functional_graph f.
Assume Hfung: functional_graph g.
Let x, y1 and y2 be given.
Assume H1: (x,y1) ∈ (f ∪ g).
Assume H2: (x,y2) ∈ (f ∪ g).
Apply (binunionE f g (x,y1) H1) to the current goal.
Assume H1f: (x,y1) ∈ f.
Apply (binunionE f g (x,y2) H2) to the current goal.
Assume H2f: (x,y2) ∈ f.
An exact proof term for the current goal is (Hfunf x y1 y2 H1f H2f).
Assume H2g: (x,y2) ∈ g.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (Hdomf x y1 H1f).
We prove the intermediate claim HxB: x ∈ B.
An exact proof term for the current goal is (Hdomg x y2 H2g).
We prove the intermediate claim HxAB: x ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B x HxA HxB).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HxAB.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE x) HxE).
Assume H1g: (x,y1) ∈ g.
Apply (binunionE f g (x,y2) H2) to the current goal.
Assume H2f: (x,y2) ∈ f.
We prove the intermediate claim HxB: x ∈ B.
An exact proof term for the current goal is (Hdomg x y1 H1g).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (Hdomf x y2 H2f).
We prove the intermediate claim HxAB: x ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B x HxA HxB).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HxAB.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((EmptyE x) HxE).
Assume H2g: (x,y2) ∈ g.
An exact proof term for the current goal is (Hfung x y1 y2 H1g H2g).
∎