proposition: Lemma nreachable_reachable n s : nreachable n s -> reachable s.
proof: Proof. intros H; elim H; clear n s H; intros; auto. apply reach0. generalize H1; clear H1; intros [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | [H1 | H1]]]]]]]]; subst s2; repeat apply reachr; repeat apply reachb; repeat apply reachd; auto. Qed.
imports: ZArith List