proposition: Lemma subterm_in_calls : forall g us, defined g R = true -> forall t, subterm_eq (Fun g us) t -> In (Fun g us) (calls t).
proof: Proof. intros g us H t. pattern t. set (Q := fun n (ts : terms n) => (exists t, Vin t ts /\ subterm_eq (Fun g us) t) -> In (Fun g us) (vcalls ts)). apply term_ind with (Q := Q); clear t. unfold subterm_eq. simpl. intros. destruct H0 as [C]. destruct C; simpl in H0; discr. intros f ts IH H0. unfold subterm_eq in H0. destruct H0 as [C]. rewrite calls_fun. pattern (defined f R). apply bool_eq_ind; intro; destruct C; simpl in H0. rewrite H0. apply in_eq. Funeqtac. subst ts. apply in_cons. apply IH. exists (fill C (Fun g us)). split. apply Vin_cast_intro. apply Vin_app_cons. unfold subterm_eq. exists C. refl. injection H0. intros. subst f. rewrite H in H1. discr. Funeqtac. subst ts. apply IH. exists (fill C (Fun g us)). split. apply Vin_cast_intro. apply Vin_app_cons. unfold subterm_eq. exists C. refl. unfold Q. simpl. intro. destruct H0 as [t]. intuition. intros t n ts H0 IH. unfold Q. simpl. intro H1. destruct H1 as [u]. do 2 destruct H1. subst u. apply in_appl. apply H0. hyp. apply in_appr. apply IH. exists u. auto. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil VecUtil EqUtil BoolUtil) Coq(Sumbool)