(n <> Cic.Anonymous && fstorder src, t) ::
aux (CicSubstitution.subst
(Deannotate.deannotate_term t) tgt) tl
- | _ -> assert false
+ | _ -> List.map (fun s -> false,s) (t::tl)
in
(false, he) :: aux hety tl
with CicTypeChecker.TypeCheckerFailure _ -> assert false