fact: Definition sumR (x y : A1 + A2) := match x, y with inl x1, inl y1 => R1 x1 y1 | inr x2, inr y2 => R2 x2 y2 | _, _ => False end.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)