An exact proof term for the current goal is (λX F x y H1 H2 ⇒ UnionI (Repl X F) y (F x) H2 (ReplI X F x H1)).