| NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
| NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
| NCic.Appl [] -> assert false
| NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
| NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
| NCic.Appl [] -> assert false
| NCic.Lambda _ | NCic.Prod _ -> [Variable]
(* I think we should CicSubstitution.subst Implicit t *)
| NCic.LetIn _ -> [Variable] (* z-reduce? *)
| NCic.Lambda _ | NCic.Prod _ -> [Variable]
(* I think we should CicSubstitution.subst Implicit t *)
| NCic.LetIn _ -> [Variable] (* z-reduce? *)