proposition: Lemma nb_aliens_fun : forall f ts, nb_aliens (Fun f ts) = if defined f R then 1 else nb_aliens_vec ts.
proof: Proof. intros. unfold nb_aliens, nb_aliens_vec. simpl. case (defined f R); refl. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)