proposition: Lemma gt2_gt1 : forall E f n (ls : Tes n) g p (us : Tes p), n <= arity (typ f) -> p <= arity (typ g) -> gt1 E (mk_call f ls) (mk_call g us) -> forall s (ts' : Tes (arity (typ f) - n)) (us' : Tes (arity (typ g) - p)) (nf : n + (arity (typ f) - n) = arity (typ f)) (pg : p + (arity (typ g) - p) = arity (typ g)), vint I (inputs (typ f)) (Vapp (Vmap (subs s) ls) ts') -> (forall x A, MapsTo x A E -> ~XSet.In x (fvs ls) -> int I A (s x)) -> gt2 (mk_max_call f (Vcast (Vapp (Vmap (subs s) ls) ts') nf)) (mk_max_call g (Vcast (Vapp (Vmap (subs s) us) us') pg)).
proof: Proof. intros E f n ls g p us hn hp hgt1 s ts' us' nf pg hlsts' hs. revert hgt1. unfold gt1, gt2, gt2c, Def.gt_call, Rof, transp; simpl. intro hgt1. inversion hgt1; clear hgt1; subst. apply left_lex. hyp. apply right_lex. left. revert H0. unfold Def.gt_args_lex, Rof. set (M := CO.filter (code g)). rewrite !lexv_eq. simpl. intros [i [i1 [i2 i3]]]. ex i i1. split. eapply opt_incl with (x := RelUtil.restrict (SN R_aeq) (clos_aeq (supterm_acc!))). apply incl_tc. unfold gt0. rewrite restrict_union. fo. inversion i2; clear i2. rewrite !Vopt_filter_cast, Vopt_filter_app with (x:=subs s x), Vopt_filter_app with (x:=subs s y). apply opt_intro. split. symmetry in H. destruct (Vnth_opt_filter_Some_elim H) as [a e]. rewrite e, <- Vnth_map. apply Vforall_nth. eapply vint_forall_sn. apply I_cp. apply not_neutral_apps_fun. eapply vint_app_term_elim_l. apply hlsts'. apply clos_aeq_tc_supterm_acc_subs. hyp. rewrite Vopt_filter_map, Vnth_map, <- H0. refl. rewrite Vopt_filter_map, Vnth_map, <- H. refl. intros j ji jg. rewrite !Vopt_filter_cast. gen (i3 _ ji jg); intro h. inversion h; clear h; subst. rewrite Vopt_filter_app with (x:=subs s x), Vopt_filter_app with (x:=subs s y). apply opt_intro. rewrite H1. refl. rewrite Vopt_filter_map, Vnth_map, <- H0. refl. rewrite Vopt_filter_map, Vnth_map, <- H. refl. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)