| C.Cast _ -> []
| C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)]
| C.Prod _ -> []
| C.Lambda (n,s,t) when t == term -> [Some (n,C.Decl s)]
| C.Lambda _ -> []
| C.Cast _ -> []
| C.Prod (n,s,t) when t == term -> [Some (n,C.Decl s)]
| C.Prod _ -> []
| C.Lambda (n,s,t) when t == term -> [Some (n,C.Decl s)]
| C.Lambda _ -> []