proposition: Lemma star_ind2 : forall x (P:A -> Prop), (P x) -> (forall y, P y -> forall z, R y z -> P z) -> forall a, star x a -> P a.
proof: Proof. intros x P H H0 a H1. induction H1. exact H. apply H0 with (y:=y);assumption. Qed.
imports: Coq(Relations Wellfounded)