proposition: Lemma in_aliens_subterm : forall u t, Vin u (aliens (capa t)) -> subterm_eq u t.
proof: Proof. intros u t. pattern t. apply term_ind_forall. simpl. intros. contr. intros f ts H. simpl. case (defined f R). simpl. intro. destruct H0. subst u. refl. contr. change (Vin u (conc (Vmap capa ts)) -> subterm_eq u (Fun f ts)). intro. assert (exists c, Vin c (Vmap capa ts) /\ Vin u (aliens c)). apply in_conc. hyp. destruct H1 as [c]. destruct H1. assert (exists t, Vin t ts /\ c = capa t). apply Vin_map. hyp. destruct H3 as [t']. destruct H3. subst c. assert (Vin u (aliens (capa t')) -> subterm_eq u t'). pattern t'. eapply Vforall_in with (n := arity f). apply H. hyp. apply subterm_strict. eapply subterm_trans_eq1 with (u := t'). apply H4. hyp. apply subterm_fun. hyp. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)