+ | Some x -> i && does_not_occur ~subst context n nn x) l true &&
+ (try
+ let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
+ does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
+ with
+ CicUtil.Subst_not_found _ -> true)