proposition: Lemma acc_star : forall A (R : relation A) a, Acc R a -> forall b, refl_trans_clos R b a -> Acc R b.
proof: Proof. intros A R a Acc_a b H; destruct H as [a1 | a1 a2 H]. assumption. apply Acc_incl with (trans_clos R). intros b1 b2 H'; apply t_step; assumption. apply Acc_inv with a2; trivial. apply acc_trans; trivial. Qed.
imports: Coq(Setoid Relations List Wellfounded)