proposition: Lemma contract_equ_pre `(c1 : contract i Ω1) `(c2 : contract i Ω2) `(equ : contract_equ c1 c2) (ω1 : Ω1) `(p : impure i a) : pre (to_hoare c1 p) ω1 <-> pre (to_hoare c2 p) (contract_iso_lr equ ω1).
proof: Proof. induction equ. revert ω1. induction p; intros ω1. + now split. + cbn. rewrite (caller_equ ω1 β e). setoid_rewrite (callee_equ ω1 β e). split. ++ intros [ocaller onext]. split; auto. intros x ω1' [ocallee owitness]. rewrite owitness. rewrite <- witness_equ. rewrite <- H; eauto. ++ intros [ocaller onext]. split; auto. intros x ω1' [ocallee owitness]. rewrite H; eauto. rewrite owitness. cbn. rewrite witness_equ. eauto. Qed.
imports: FreeSpec.Core(Interface ImpureFacts Contract)