proposition: Lemma in_calls_defined : forall t g vs, In (Fun g vs) (calls t) -> defined g R = true.
proof: Proof. intros. ded (in_calls H). do 3 destruct H0. injection H0. intros. subst x. hyp. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil VecUtil EqUtil BoolUtil) Coq(Sumbool)