proposition: Lemma triple_conj: forall c P1 Q1 P2 Q2, {{P1}} c {{Q1}} -> {{P2}} c {{Q2}} -> {{P1 //\\ P2}} c {{Q1 //\\ Q2}}.
proof: Proof. intros; red; intros. destruct H2 as [PRE1 PRE2]. split; eauto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)