proposition: Lemma one_step_list_incl : forall A (R1 R2 : relation A), (forall a1 a2, R1 a1 a2 -> R2 a1 a2) -> forall l1 l2, one_step_list R1 l1 l2 -> one_step_list R2 l1 l2.
proof: Proof. intros A R1 R2 R1_in_R2. fix one_step_list_incl 1. intros l1; case l1; clear l1. intros l2 H; inversion H. intros a1 l1 l2 H; inversion H as [b1 b2 l H1 | b k1 k2 Hk]; subst. left; apply R1_in_R2; assumption. right; apply one_step_list_incl; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)