proposition: Lemma contract_equ_sym `(c1 : contract i Ω1) `(c2 : contract i Ω2) (equ : contract_equ c1 c2) : contract_equ c2 c1.
proof: Proof. induction equ. apply mk_contract_equ with (f0:=g) (g0:=f). + apply iso2. + apply iso1. + intros ω α p. transitivity (caller_obligation c2 (f (g ω)) p). ++ now rewrite iso1. ++ now symmetry. + intros ω α p x. transitivity (callee_obligation c2 (f (g ω)) p x). ++ now rewrite iso1. ++ now symmetry. + intros ω α p x. rewrite <- (iso2 (witness_update c1 (g ω) p x)). assert (equ : witness_update c2 ω p x = f (witness_update c1 (g ω) p x)). { transitivity (witness_update c2 (f (g ω)) p x). + now rewrite iso1. + now rewrite witness_equ. } now rewrite equ. Defined.
imports: Coq(Setoid Morphisms) ExtLib(StateMonad MonadState MonadTrans) FreeSpec.Core(Interface Impure Semantics Component)