proposition: Lemma do_coherent : coherent do_sp.
proof: Proof. case=>q H y m; split. - by case=>i [/= H1 T1]; exists i; exists H1; exists i. by case=>i [/= H1][_][<-] T1; exists i. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)