(match List.nth context (n-1) with
Some (_,C.Decl _) -> true
| Some (_,C.Def (bo,_)) ->
(match List.nth context (n-1) with
Some (_,C.Decl _) -> true
| Some (_,C.Def (bo,_)) ->
| Cic.Variable (_,None,_,_) -> ()
| _ ->
raise (TypeCheckerFailure
| Cic.Variable (_,None,_,_) -> ()
| _ ->
raise (TypeCheckerFailure