proposition: Lemma subterm_eq_sub_elim : forall u t s, subterm_eq t (sub s u) -> exists v, subterm_eq v u /\ match v with | Var x => subterm_eq t (s x) | Fun f ts => t = sub s v end.
proof: Proof. intro u; pattern u; apply term_ind_forall; clear u. intros x t s ht. exists (Var x). intuition. intros f ts IH t s ht. destruct (subterm_eq_split ht). exists (Fun f ts). intuition. destruct (subterm_fun_elim H) as [v [hv1 hv2]]. change (Vin v (Vmap (sub s) ts)) in hv1. destruct (Vin_map hv1) as [w [hw1 hw2]]. subst. destruct (Vforall_in IH hw1 t s hv2) as [x [hx1 hx2]]. exists x. split. trans w. hyp. apply subterm_strict. apply subterm_fun. hyp. hyp. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)