proposition: Lemma gt_args_lex_absorbs_gt_red R S r : Proper (aeq ==> aeq ==> impl) S -> Transitive S -> restrict (SN (clos_aeq R)) (clos_aeq R) << S -> gt_args_lex S r @ gt_red R << gt_args_lex S r.
proof: Proof. intros S_aeq S_trans RS [f n ts] [g' p' vs] [[g p us] [h1 h2]]. inv_gt_red h2 g' p'. destruct h0 as [us' [usus' [vs' [h0 vs'vs]]]]. rewrite Vrel1_nth_iff in h0. destruct h0 as [j [j1 [j2 j3]]]. assert (a : S (Vnth us j1) (Vnth vs j1)). apply RS. split. apply sn_clos_vaeq_elim. hyp. eapply clos_aeq_intro. 3: apply j2. apply Vforall2_elim_nth. hyp. apply Vforall2_elim_nth. hyp. revert h1. unfold Def.gt_args_lex, Rof. simpl. set (M := CO.filter r). rewrite !lexv_eq. intros [i [i1 [i2 i3]]]. case_eq (Vfirst_position (eq_nat_dec j) M). intros k hk. destruct (lt_dec k i). assert (kr : k < filter_arity r). lia. ex k kr. split. gen (i3 _ l kr). rewrite !Vnth_opt_filter, <- (Vnth_first_position (eq_nat_dec j) hk). destruct (lt_dec j n); destruct (lt_dec j p); try lia; intro i3k; inversion i3k; clear i3k; subst; apply opt_intro. rewrite H1, Vnth_eq with (h2:=j1), Vnth_eq with (h1:=l1) (h2:=j1); auto. intros m mk mr. assert (mi : m < i). lia. gen (i3 _ mi mr). rewrite !Vnth_opt_filter. set (q := Vnth M mr). destruct (lt_dec q n); destruct (lt_dec q p); try lia; intro i3k; inversion i3k; clear i3k; subst; apply opt_intro. rewrite H1, (Vforall2_elim_nth _ usus'), <- (Vforall2_elim_nth _ vs'vs), j3. refl. intro b. symmetry in b. gen (Vfirst_position_nth (eq_nat_dec j) hk b). lia. ex i i1. split. revert i2. rewrite !Vnth_opt_filter. set (q := Vnth M i1). destruct (lt_dec q n); destruct (lt_dec q p); intro i2; inversion i2; clear i2; subst; apply opt_intro. destruct (eq_nat_dec k i). subst. assert (b : j = q). eapply Vnth_first_position. apply hk. rewrite !Vnth_eq with (h1:=j1) (h2:=l0) in a; auto. apply S_trans with (Vnth us l0); hyp. rewrite <- (Vforall2_elim_nth _ vs'vs), <- j3, <- (Vforall2_elim_nth _ usus'). hyp. intro b. symmetry in b. gen (Vfirst_position_nth (eq_nat_dec j) hk b). lia. intros m mi mr. gen (i3 _ mi mr). rewrite !Vnth_opt_filter. set (q := Vnth M mr). destruct (lt_dec q n); destruct (lt_dec q p); try lia; intro i3k; inversion i3k; clear i3k; subst; apply opt_intro. rewrite H1, (Vforall2_elim_nth _ usus'), <- (Vforall2_elim_nth _ vs'vs), j3. refl. intro b. symmetry in b. gen (Vfirst_position_nth (eq_nat_dec j) hk b). lia. ex i i1. split. revert i2. rewrite !Vnth_opt_filter. set (q := Vnth M i1). destruct (lt_dec q n); destruct (lt_dec q p); intro i2; inversion i2; clear i2; subst; apply opt_intro. rewrite <- (Vforall2_elim_nth _ vs'vs), <- j3, <- (Vforall2_elim_nth _ usus'). hyp. intro. subst j. assert (b : Vin q M). apply Vnth_in. destruct (Vin_first_position eq_nat_dec b) as [i0 hi0]. rewrite H in hi0. discr. intros m mi mr. gen (i3 _ mi mr). rewrite !Vnth_opt_filter. set (q := Vnth M mr). destruct (lt_dec q n); destruct (lt_dec q p); try lia; intro i3k; inversion i3k; clear i3k; subst; apply opt_intro. rewrite H2, (Vforall2_elim_nth _ usus'), <- (Vforall2_elim_nth _ vs'vs), j3. refl. intro. subst j. assert (b : Vin q M). apply Vnth_in. destruct (Vin_first_position eq_nat_dec b) as [i0 hi0]. rewrite H in hi0. discr. Qed.
imports: Coq(Morphisms Basics Lexicographic_Product) CoLoR(LogicUtil LSimple VecUtil RelUtil VecOrd EqUtil Lexico SN NatUtil)