eat_branch (pred n) rels t pat
| NCic.Prod (_, _, t), NCic.Lambda (name, s, t') ->
let cv, rhs = eat_branch 0 ((mk_id name)::rels) t t' in
eat_branch (pred n) rels t pat
| NCic.Prod (_, _, t), NCic.Lambda (name, s, t') ->
let cv, rhs = eat_branch 0 ((mk_id name)::rels) t t' in