proposition: Lemma gt2_clos_vaeq : forall f (ts us : TypArgs f), vint I (inputs (typ f)) ts -> ts ==>R us -> gt2 (mk_max_call f ts) (mk_max_call f us).
proof: Proof. intros f ts us hts tsus. unfold gt2, gt2c, Def.gt_call, Rof, transp. apply right_lex. unfold Def.gt_args_lex, Rof. red. simpl. right. apply gt_red_intro. fo. apply sn_clos_vaeq_intro. eapply vint_forall_sn. apply I_cp. apply not_neutral_apps_fun. apply hts. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)