proposition: Lemma to_hoare_contractprod `{Provide ix i, Provide ix j} `(ci : contract i Ωi) `(cj : contract j Ωj) `(p : impure ix a) `(prei : pre (to_hoare ci p) ωi) `(prej : pre (to_hoare cj p) ωj) : pre (to_hoare (ci * cj) p) (ωi, ωj).
proof: Proof. revert ωi prei ωj prej. induction p; intros ωi prei ωj prej. + auto. + destruct prei as [calleri Hcalleei]. destruct prej as [callerj Hcalleej]. split. ++ now split. ++ intros x [ωi' ωj'] [[calleei calleej] equωs]. cbn in equωs. inversion equωs; subst. apply H3. +++ apply Hcalleei. now split. +++ apply Hcalleej. now split. Qed.
imports: FreeSpec.Core(Interface ImpureFacts Contract)