proposition: Lemma contract_equ_post `(c1 : contract i Ω1) `(c2 : contract i Ω2) `(equ : contract_equ c1 c2) (ω1 ω1' : Ω1) `(p : impure i a) (x : a) (post1 : post (to_hoare c1 p) ω1 x ω1') : post (to_hoare c2 p) (contract_iso_lr equ ω1) x (contract_iso_lr equ ω1').
proof: Proof. induction equ. cbn in *. revert x ω1 ω1' post1. induction p; intros y ω1 ω1' post1. + destruct post1 as [xequ ω1equ]. cbn. now subst. + cbn in post1. destruct post1 as [x [ω1'' [[ocallee owitness] post1]]]. eapply H in post1. exists x. exists (f ω1''). split; auto. cbn. repeat split. ++ eapply callee_equ; eauto. ++ rewrite owitness. apply witness_equ. Qed.
imports: FreeSpec.Core(Interface ImpureFacts Contract)