proposition: Lemma in_calls : forall x t, In x (calls t) -> exists g, exists vs, x = Fun g vs /\ defined g R = true.
proof: Proof. intros x t. pattern t. set (Q := fun n (ts : terms n) => In x (vcalls ts) -> exists g, exists vs, x = Fun g vs /\ defined g R = true). apply term_ind with (Q := Q); clear t. simpl. intros. contr. intros f ts IH. rewrite calls_fun. pattern (defined f R). apply bool_eq_ind; simpl; intros. destruct H0. exists f. exists ts. auto. apply IH. hyp. apply IH. hyp. unfold Q. simpl. intro. contr. unfold Q. simpl. intros. ded (in_app_or H1). intuition. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil VecUtil EqUtil BoolUtil) Coq(Sumbool)