proposition: Lemma fill_var_elim : forall x c d (u : term), fill c (Var x) = fill d u -> exists e, c = comp d e.
proof: Proof. induction c. simpl. intros. destruct (var_eq_fill H). subst. exists Hole. refl. simpl. intros. destruct (fun_eq_fill H). subst. exists (Cont f e t c t0). refl. decomp H0. subst. simpl in *. Funeqtac. arity. arity. simpl Vapp in *. assert (x2=e). apply eq_unique. subst x2. rewrite Vcast_eq in H0. inversion H0. destruct (IHc _ _ H3). subst. exists x0. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)