proposition: Lemma union_rel_func : functional R -> functional S -> fcompatible -> functional Union_rel.
proof: Proof. move=> fR fS fC x y1 y2; case=> [hR1 | hS1]; case=> [hR2 | hS2]. - by apply: fR hR1 hR2. - apply: fC hR1 hS2. - apply/esym; apply: fC hR2 hS1. by apply: fS hS1 hS2. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)