proposition: Lemma filt_nullP (q : pred ptr) : null \notin supp f -> null \notin supp (kfilter q f).
proof: Proof. by move=>H; rewrite supp_kfilt mem_filter negb_and H orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)