proposition: Lemma sepconj_emp: forall P, emp ** P = P.
proof: Proof. intros; apply assertion_extensionality; intros; split. - intros (h1 & h2 & EMP1 & P2 & EQ & DISJ). red in EMP1. subst h h1. rewrite hunion_empty; auto. - intros. exists hempty, h; intuition auto. red; auto. red; auto. rewrite hunion_empty; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)