proposition: Lemma st_botP e : st_leq st_bot e.
proof: Proof. by case: e=>p e S D F; exists (@pred_topP _ _)=>???; apply: botP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)