proposition: Lemma compat_hd_red : forall R, substitution_closed succ -> compat R -> hd_red R << succ.
proof: Proof. unfold inclusion. intros. redtac. subst x. subst y. apply H. apply H0. hyp. Qed.
imports: CoLoR(ATrs RelUtil ListUtil ARelation SN LogicUtil)