proposition: Lemma calls_fun : forall f ts, calls (Fun f ts) = match defined f R with | true => Fun f ts :: vcalls ts | false => vcalls ts end.
proof: Proof. intros. refl. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil VecUtil EqUtil BoolUtil) Coq(Sumbool)