let context = (name,NCic.Decl ty)::context in
eat_branch 0 t context ctx t'
| Forall (_,_,t),NCic.Lambda (name, ty, t') ->
let ctx =
let context = (name,NCic.Decl ty)::context in
eat_branch 0 t context ctx t'
| Forall (_,_,t),NCic.Lambda (name, ty, t') ->
let ctx =