proposition: Lemma int_red_rtc_preserve_hd : forall u v, int_red R # u v -> u=v \/ exists f us vs, u = Fun f us /\ v = Fun f vs.
proof: Proof. intros. induction H; auto. right. apply int_red_preserve_hd. auto. destruct IHclos_refl_trans1; destruct IHclos_refl_trans2; subst; auto. right. do 3 destruct H1. do 3 destruct H2. split_all. subst. Funeqtac. subst. ex x0 x1 x5. auto. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)