proposition: Lemma list_cell_local_facts: forall {cs: compspecs} {list_structid list_link: ident}{list_token} (ls: listspec list_structid list_link list_token) sh v p, list_cell ls sh v p |-- !! field_compatible list_struct nil p.
proof: Proof. intros. unfold list_cell. normalize. Qed.
imports: VST.floyd.base2 VST.floyd.client_lemmas VST.floyd.closed_lemmas VST.floyd.nested_pred_lemmas VST.floyd.nested_field_lemmas VST.floyd.efield_lemmas VST.floyd.mapsto_memory_block VST.floyd.reptype_lemmas VST.floyd.data_at_rec_lemmas VST.floyd.field_at VST.floyd.nested_loadstore VST.floyd.entailer