proposition: Lemma struct_pred_type_changable: forall m m' A F v v' p p', m=m' -> JMeq v v' -> (forall it v, F it v p = F it v p') -> @struct_pred m A F v p = @struct_pred m' A F v' p'.
proof: Proof. intros. subst m'. apply JMeq_eq in H0. subst v'. induction m. reflexivity. destruct m. destruct a; simpl; apply H1. rewrite !struct_pred_cons2. f_equal. auto. apply IHm. 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