proposition: Lemma red_case : forall t u, red R t u -> hd_red R t u \/ exists f ts i (p : i < arity f) u', t = Fun f ts /\ red R (Vnth ts p) u' /\ u = Fun f (Vreplace ts p u').
proof: Proof. intros. redtac. destruct c. left. subst. simpl. apply hd_red_rule. hyp. right. ex f (Vcast (Vapp t0 (Vcons (fill c (sub s l)) t1)) e) i. assert (p : i<arity f). lia. ex p (fill c (sub s r)). subst. simpl. split_all. rewrite Vnth_cast, Vnth_app. destruct (le_gt_dec i i). 2: lia. rewrite Vnth_cons_head. apply red_rule. hyp. lia. apply args_eq. apply Veq_nth; intros. rewrite Vnth_cast, Vnth_app. destruct (le_gt_dec i i0). destruct (eq_nat_dec i i0). subst i0. rewrite Vnth_cons_head, Vnth_replace. refl. lia. rewrite Vnth_replace_neq. 2: hyp. rewrite Vnth_cast, Vnth_app. destruct (le_gt_dec i i0). 2: lia. assert (l0=l1). apply le_unique. subst l1. rewrite !Vnth_cons. destruct (lt_ge_dec 0 (i0-i)). apply Vnth_eq. refl. lia. rewrite Vnth_replace_neq. 2: lia. rewrite Vnth_cast, Vnth_app. destruct (le_gt_dec i i0). lia. apply Vnth_eq. refl. Qed.
imports: CoLoR(ARelation ListNodup LogicUtil VecUtil RelUtil ListUtil SN BoolUtil EqUtil NatUtil ListMax VecOrd) Coq(Morphisms)