proposition: Lemma sub_capa : forall t, fcap_aliens (capa t) = t.
proof: Proof. intro. pattern t. apply term_ind_forall; intros. refl. unfold fcap_aliens, fcap, aliens. simpl. case (defined f R); simpl. refl. apply args_eq. change (Vmap_sum (Vmap capa v) (conc (Vmap capa v)) = v). rewrite Vmap_sum_conc_forall. refl. hyp. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)