proposition: Lemma red_split : forall t u, red R t u -> hd_red R t u \/ int_red R t u.
proof: Proof. intros t u tu. redtac. destruct c; subst. left. apply hd_red_rule. hyp. right. ex l r (Cont f e t0 c t1) s. split_all. discr. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)