proposition: Lemma int_red_fun : forall f ts v, int_red R (Fun f ts) v -> exists i (vi : terms i) t j (vj : terms j) h t', ts = Vcast (Vapp vi (Vcons t vj)) h /\ v = Fun f (Vcast (Vapp vi (Vcons t' vj)) h) /\ red R t t'.
proof: Proof. intros. redtac. destruct c. absurd (@Hole Sig = Hole); auto. simpl in xl. Funeqtac. ex i t (fill c (sub s l)) j t0 e (fill c (sub s r)). split. hyp. split. hyp. unfold red. ex l r c s. auto. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)