proposition: Lemma Vgt_prod_fun : forall f ts ts', Vrel1 (red R) ts ts' -> int_red R (Fun f ts) (Fun f ts').
proof: Proof. intros. ded (Vrel1_app_impl H). do 8 destruct H0. destruct H1. redtac. subst x1. subst x5. unfold transp, int_red. rewrite H0, H1. ex l r (Cont f x4 x0 c x3) s. split. discr. auto. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)