proposition: Lemma int_red_pos_eq : forall R, int_red_pos R == int_red R.
proof: Proof. intro R. split; intros t u tu. destruct tu as [i [f [hi [ts [e [v [h1 h2]]]]]]]. redtac. subst. ex l r. assert (l1 : 0 + i <= arity f). lia. set (v1 := Vsub ts l1). assert (l2 : S i + (arity f - S i) <= arity f). lia. set (v2 := Vsub ts l2). assert (l3 : i + S (arity f - S i) = arity f). lia. ex (Cont f l3 v1 c v2) s. split_all. discr. simpl. apply args_eq. apply Veq_nth. intros j hj. rewrite Vnth_cast, Vnth_app. destruct (le_gt_dec i j). rewrite Vnth_cons. destruct (lt_ge_dec 0 (j-i)). unfold v2. rewrite Vnth_sub. apply Vnth_eq. clear -l4; lia. assert (j=i). clear -l0 g; lia. subst. rewrite (lt_unique _ hi). hyp. unfold v1. rewrite Vnth_sub. apply Vnth_eq. refl. simpl. apply args_eq. apply Veq_nth. intros j hj. rewrite Vnth_cast, Vnth_app. destruct (le_gt_dec i j). rewrite Vnth_cons. destruct (lt_ge_dec 0 (j-i)). rewrite Vnth_replace_neq. 2: clear -l4; lia. unfold v2. rewrite Vnth_sub. apply Vnth_eq. clear -l4; lia. assert (j=i). clear -l0 g; lia. subst. apply Vnth_replace. rewrite Vnth_replace_neq. 2: clear -g; lia. unfold v1. rewrite Vnth_sub. apply Vnth_eq. refl. redtac. subst. destruct c. cong. ex i f. assert (hi : i < arity f). lia. exists hi. simpl. exists (Vcast (Vapp t (Vcons (fill c (sub s l)) t0)) e). split_all. exists (fill c (sub s r)). split. rewrite Vnth_cast, Vnth_app. destruct (le_gt_dec i i). rewrite Vnth_cons. destruct (lt_ge_dec 0 (i-i)). lia. apply red_rule. hyp. lia. apply args_eq. apply Veq_nth. intros k hk. rewrite Vnth_cast, Vnth_app. case_eq (le_gt_dec i k); intros l0 H. rewrite Vnth_cons. case_eq (lt_ge_dec 0 (k-i)); intros l1 H0. rewrite Vnth_replace_neq, Vnth_cast, Vnth_app, H, Vnth_cons, H0. refl. lia. assert (k=i). lia. subst. sym. apply Vnth_replace. rewrite Vnth_replace_neq, Vnth_cast, Vnth_app, H. refl. lia. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)