proposition: Lemma one_step_incl : forall (R1 R2 : term -> term -> Prop) , (forall t1 t2, R1 t1 t2 -> R2 t1 t2) -> forall t1 t2, one_step R1 t1 t2 -> one_step R2 t1 t2.
proof: Proof. intros R1 R2 Incl t1; pattern t1; apply term_rec3; clear t1. intros x1 t2 H; inversion H; apply at_top; apply axiom_incl with R1; trivial. intros f1 l1 Hrec t2 H; inversion_clear H as [| f l1' l2 H']. apply at_top; apply axiom_incl with R1; trivial. apply in_context; generalize l2 H'; clear l2 H'; induction l1 as [ | a1 l1 ]; intros l2 H; inversion_clear H. apply head_step; apply Hrec; trivial; left; trivial. apply tail_step; apply IHl1; trivial; intros; apply Hrec; trivial; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)