fact: Definition lift_eq (u v : lift A) := match u, v with up a, up b => a == b | down, down => true | _, _ => false end.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype) pcm(options prelude) pcm(pcm morphism)