proposition: Lemma pred_sepcon_strong_proper: forall P1 P2 p1 p2, (forall x, P1 x <-> P2 x) -> (forall x, P1 x -> P2 x -> p1 x = p2 x) -> pred_sepcon P1 p1 = pred_sepcon P2 p2.
proof: Proof. assert (forall P1 P2 p1 p2, (forall x, P1 x <-> P2 x) -> (forall x, P1 x -> P2 x -> p1 x = p2 x) -> pred_sepcon P1 p1 |-- pred_sepcon P2 p2). 2: intros; apply pred_ext; apply H; [auto | auto | symmetry; auto | symmetry; auto]. intros. unfold pred_sepcon. apply exp_left; intro l; apply (exp_right l). normalize. assert (forall x : B, In x l <-> P2 x) by (intros; rewrite H1, H; reflexivity). normalize. erewrite iter_sepcon_func_strong; [apply derives_refl |]. intros. specialize (H1 x); specialize (H3 x). apply H0; tauto. Qed.
imports: CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.List_ext VST.msl.Extensionality VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.Morphisms CertiGraph.msl_ext.seplog CertiGraph.msl_ext.log_normalize