-(* VERSIONE ERRATA
- | Cic.Appl (h1::l),Cic.Appl (h2::l') when h1 = h2 ->
- let rc = check_subsumed b t1 t1 in
- if rc then
- true, true
- else if h1 = h2 then
- (try
- List.fold_left2
- (fun (ok_so_far, subsumption_used) t t' ->
- aux true (ok_so_far, subsumption_used) t t')
- (ok_so_far, subsumption_used) l l'
- with Invalid_argument _ -> false,subsumption_used)
- else
- false, subsumption_used
- | _ -> false, subsumption_used *)