fact: Definition SingleFrame'_inv {l g s s0} (F: SingleFrame' l g (Ssequence s s0)) : SingleFrame' l g s := match F with | RAM_FRAME.Build_SingleFrame' f cont fs => RAM_FRAME.Build_SingleFrame' f (Ssequence s0 cont) fs end.
imports: CertiGraph.lib.Ensembles_ext CertiGraph.lib.Relation_ext CertiGraph.lib.List_ext CertiGraph.veric_ext.SeparationLogic CertiGraph.floyd_ext.ramification VST.floyd.base VST.floyd.canon VST.floyd.assert_lemmas VST.floyd.client_lemmas VST.floyd.closed_lemmas