proposition: Lemma fun_eq_nth_fill : forall f v i (h : i < arity f), let v1 := Vsub v (Veq_app_cons_aux1 h) in let v2 := Vsub v (Veq_app_cons_aux2 h) in let H := Veq_app_cons_aux3 h in let c := Cont H v1 Hole v2 in Fun f v = fill c (Vnth v h).
proof: Proof. intros. simpl. apply args_eq. apply Veq_nth; intros j Hj. rewrite Vnth_cast, Vnth_app. case (le_gt_dec i j); intros. 2:{ unfold v1. rewrite Vnth_sub. apply Vnth_eq. refl. } rewrite Vnth_cons. destruct (lt_ge_dec 0 (j-i)). unfold v2. rewrite Vnth_sub. apply Vnth_eq. lia. apply Vnth_eq. lia. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)