proposition: Lemma comp_Ews_not_bot: Share.comp Ews <> Share.bot.
proof: Proof. intro. apply (f_equal Share.comp) in H. rewrite comp_bot in H. rewrite Share.comp_inv in H. unfold Ews in H. unfold extern_retainer in H. pose proof fun x1 x2 => split_nontrivial' x1 x2 Share.Lsh. pose proof fun x1 x2 => split_join x1 x2 Share.Lsh. destruct (Share.split Share.Lsh) as [sh1 sh2]; simpl in H. specialize (H0 _ _ eq_refl). specialize (H1 _ _ eq_refl). pose proof fun HH => Lsh_nonidentity (H0 HH); clear H0. assert (sh1 = Share.Lsh). { pose proof glb_Rsh_Lsh. pose proof @sub_glb_bot Share.Rsh sh1 Share.Lsh ltac:(eapply sepalg.join_join_sub; eauto) H0. pose proof lub_Lsh_Rsh. rewrite Share.lub_commute in H. rewrite Share.lub_commute in H4. apply (Share.distrib_spec Share.Rsh sh1 Share.Lsh); congruence. } apply H2; right; clear H2. subst sh1. pose proof sepalg.join_assoc H1 H1 as [sh22 [? ?]]. apply sepalg.join_self in H0. auto. Qed.
imports: CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin VST.veric.SeparationLogic CertiGraph.copy.env_copy_bin