proposition: Lemma reachable_valid s : reachable s -> valid_state s.
proof: Proof. intros H; elim H; auto. - apply valid_state_init. - intros; apply valid_state_right; auto. - intros; apply valid_state_back; auto. - intros; apply valid_state_down; auto. Qed.
imports: ZArith List