proposition: Lemma legal_trans : forall (x : Z) (c c' : Config), legal x c -> legal (co c) c' -> legal x c'.
proof: Proof. intros; elim H0. unfold mk_init_config in |- *; rewrite simpl_config; trivial. intros; apply after; trivial. Qed.
imports: ZArith Omega