+ (* DEBUG
+ let t1 = CicMetaSubst.subst subst hete t in
+ let t2 = CicSubstitution.subst hete t in
+ prerr_endline ("con subst = " ^(CicPp.ppterm t1));
+ prerr_endline ("senza subst = " ^(CicPp.ppterm t2));
+ prerr_endline("++++++++++metasenv prima di eat_prods:\n" ^
+ (CicMetaSubst.ppmetasenv metasenv subst));
+ prerr_endline("++++++++++subst prima di eat_prods:\n" ^
+ (CicMetaSubst.ppsubst subst));
+ *)
+ eat_prods metasenv subst context
+ (* (CicMetaSubst.subst subst hete t) tl *)
+ (CicSubstitution.subst hete t) tl