proposition: Lemma llist_null A (xs : seq A) h : valid h -> llist null xs h -> xs = [::] /\ h = Unit.
proof: Proof. case: xs=>[|x xs] /= V H; first by case: H. by case: H V=>p [h'][-> _] /validPtUn_cond. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)