proposition: Lemma in_calls_subterm : forall u t, In u (calls t) -> subterm_eq u t.
proof: Proof. intros u t. pattern t. set (Q := fun n (ts : terms n) => In u (vcalls ts) -> exists t, Vin t ts /\ subterm_eq u t). apply term_ind with (Q := Q); clear t. simpl. intros. contr. intros f ts IH. rewrite calls_fun. case (defined f R); simpl; intro. destruct H. rewrite H. refl. ded (IH H). destruct H0 as [t]. destruct H0. apply subterm_strict. eapply subterm_trans_eq1. apply H1. apply subterm_fun. hyp. ded (IH H). destruct H0 as [t]. destruct H0. apply subterm_strict. eapply subterm_trans_eq1. apply H1. apply subterm_fun. hyp. unfold Q. simpl. intros. contr. unfold Q. simpl. intros. ded (in_app_or H1). destruct H2. ded (H H2). exists t. auto. ded (H0 H2). destruct H3 as [w]. destruct H3. exists w. auto. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil VecUtil EqUtil BoolUtil) Coq(Sumbool)