fact: Definition revT : Type := forall p, STsep (fun i => exists ps, i \In shape_rev p ps, fun y i m => forall ps, i \In shape_rev p ps -> exists r, m \In lseq r (rev ps.1 ++ ps.2) /\ y = Val r).
imports: mathcomp(ssreflect ssrbool eqtype seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep stlogR)