+ with Invalid_argument _ -> assert false in
+ let rec check_non_linear_patterns =
+ function
+ [] -> true
+ | (name,t)::tl ->
+ List.for_all
+ (fun (name',t') ->
+ name <> name' ||
+ CicUtil.alpha_equivalence
+ (Deannotate.deannotate_term t) (Deannotate.deannotate_term t')
+ ) tl && check_non_linear_patterns tl