proposition: Lemma last_successor_is_last : forall y0 y : legal_config, ~ no_copy_succ y (last_successor y0).
proof: Proof. intros. unfold last_successor in |- *. apply root_no_R. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8