proposition: Lemma imp_prop_ext: forall {A} {NA: NatDed A} (P P' :Prop) (Q Q': A), (P <-> P') -> (P -> Q = Q') -> !!P --> Q = !!P' --> Q'.
proof: Proof. intros. apply pred_ext. + apply imp_andp_adjoint. normalize. rewrite prop_imp by tauto. rewrite H0 by tauto. auto. + apply imp_andp_adjoint. normalize. rewrite prop_imp by tauto. rewrite H0 by tauto. auto. Qed.
imports: VST.msl.Extensionality VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize Coq.Lists.List CertiGraph.msl_ext.seplog CertiGraph.msl_ext.abs_addr