proposition: Lemma localV U f x y r : @local_fun U f -> valid (x \+ y) -> f x y = Some r -> valid (r \+ y).
proof: Proof. by move=>H V E; move: (H Unit x y r); rewrite unitL !unitR; case. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)