[STATEMENT]
lemma accessible_on_restrict_to_downwards:
  assumes "(restrict_to P A)\<^sup>+\<^sup>+ a b" and "accessible_on P A b"
  shows "accessible_on P A a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accessible_on P A a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(restrict_to P A)\<^sup>+\<^sup>+ a b
accessible_on P A b

goal (1 subgoal):
 1. accessible_on P A a
[PROOF STEP]
by (induct) (auto dest: accessible_on_imp_mem accessible_on_downward)