proposition: Lemma fill_sub n f i vi j vj e s l : n >= maxvar l -> fill (Cont f e vi Hole vj) (sub s l) = sub (maxvar_union (S n) s (fsub n (Vapp vi vj))) (fill (Cont f e (fresh (S n) i) Hole (fresh (S n+i) j)) l).
proof: Proof. intro. rename H into Hn. simpl. apply args_eq. rewrite Vmap_cast, Vmap_app. simpl. apply Vcast_eq_intro. apply Vapp_eq_intro. apply Veq_nth; intros. rewrite Vnth_map, Vnth_fresh. simpl. unfold maxvar_union. case (lt_ge_dec (S(n+i0)) (S n)); intro. lia. unfold fsub. case (le_lt_dec (S(n+i0)) n); intro. lia. case (le_lt_dec (S(n+i0)) (n+(i+j))); intro. rewrite Vnth_app. case (le_gt_dec i (S(n+i0)-n-1)); intro. lia. apply Vnth_eq. clear; lia. lia. apply Vcons_eq_intro. apply sub_eq. intros. ded (vars_max H). unfold maxvar_union. case (lt_ge_dec x (S n)); intro. refl. lia. apply Veq_nth; intros. rewrite Vnth_map, Vnth_fresh. simpl. unfold maxvar_union. case (lt_ge_dec (S(n+i+i0)) (S n)); intro. lia. unfold fsub. case (le_lt_dec (S(n+i+i0)) n); intro. lia. case (le_lt_dec (S(n+i+i0)) (n+(i+j))); intro. rewrite Vnth_app. case (le_gt_dec i (S(n+i+i0)-n-1)); intro. apply Vnth_eq. clear; lia. lia. lia. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)