proposition: Lemma lift_chainP : chain_axiom [Pred x : T | x = bot \/ x \In s].
proof: Proof. case: s=>p [[d H1] H2] /=; split=>[|x y]; first by exists d; right. by case=>[->|H3][->|H4]; auto. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)