proposition: Lemma synt_wp_conj: forall (p: ImpProg) (post1 post2: Pred) e, (synt_wp p post1 e) -> (synt_wp p post2 e) -> (synt_wp p (fun e => post1 e /\ post2 e) e).
proof: Proof. induction p; simpl; try ((intuition auto); fail). intros post1 post2 e H1 H2. intros; eapply synt_wp_monotonic. 2: apply (IHp1 _ _ _ H1 H2). simpl; intuition auto. intros post1 post2 e H1 H2. dec2 inv1 H1. dec2 R1 H1. dec2 inv2 H2. intros; constructor 1 with (x:=fun e => inv1 e /\ inv2 e). constructor 1 with (x:=R1). firstorder auto. Qed.
imports: hoarelogicsemantics