proposition: Lemma copy_trans_st_rt : forall s0 : Site, s0 <> owner -> access s1 (rt c0) -> ((st c0 s0 > 0)%Z -> rt c0 s0 = true) -> (st (copy_trans c0 s1 s2) s0 > 0)%Z -> rt (copy_trans c0 s1 s2) s0 = true.
proof: Proof. intro; rewrite copy_trans_st; simpl in |- *; case (eq_site_dec s0 s1); intro. unfold access in |- *; rewrite <- e; intros; elim H0; intro. absurd (s0 = owner); trivial. trivial. auto. Qed.
imports: init table_act mess_act