proposition: Lemma replace_pos_elim : forall p t u t', replace_pos t p u = Some t' -> {C | context_pos t p = Some C /\ t' = fill C u}.
proof: Proof. induction p; intros. exists Hole. simpl. destruct t; inversion H; auto. destruct t; destruct t'. discr. discr. revert H. simpl. destruct (lt_ge_dec a (arity f)); intro. destruct (replace_pos (Vnth t l) p u); inversion H. discr. gen H. simpl. destruct (lt_ge_dec a (arity f)); intro. 2: discr. destruct (replace_pos (Vnth t l) p u). 2: discr. apply Some_eq in H0. Funeqtac. subst t0. destruct (IHp (Vnth t l) u t1). revert H. simpl. destruct (lt_ge_dec a (arity f)); intro. 2: discr. assert (l0 = l). apply lt_unique. subst l0. destruct (replace_pos (Vnth t l) p u). 2: discr. f_equal. apply Some_eq in H. Funeqtac. apply Vreplace_eq_elim in H0. hyp. destruct a0. rewrite H0. exists (Cont f (Veq_app_cons_aux3 l) (Vsub t (Veq_app_cons_aux1 l)) x (Vsub t (Veq_app_cons_aux2 l))). intuition. simpl. apply args_eq. assert (fill x u = Vnth (Vreplace t l t1) l). rewrite <- H1. rewrite Vnth_replace. refl. rewrite H2. rewrite (Veq_app_cons_aux (Vreplace t l t1) (Veq_app_cons_aux1 l) l (Veq_app_cons_aux2 l) (Veq_app_cons_aux3 l)). apply Vcast_eq_intro. apply Vapp_eq_intro. rewrite Vsub_replace_l. refl. lia. apply Vcons_eq_intro. rewrite Vnth_cast. rewrite Vnth_app_cons. refl. rewrite Vsub_replace_r. refl. lia. Defined.
imports: CoLoR(ATrs ListUtil NatUtil VecUtil LogicUtil OptUtil)