+ let eq_kind, what =
+ match where with
+ | None
+ | Some ([], None) ->
+ PER.alpha_equivalence, [t1']
+ | Some (hp_paths, goal_path) ->
+ assert (hp_paths = []);
+ match goal_path with
+ | None -> assert false (* (==), [t1'] *)
+ | Some path ->
+ let roots = ProofEngineHelpers.select ~term:gty' ~pattern:path in
+ let subterms =
+ List.fold_left (
+ fun acc (i, r) ->
+ let wanted = CicSubstitution.lift (List.length i) t1' in
+ PEH.find_subterms ~eq:PER.alpha_equivalence ~wanted r @ acc
+ ) [] roots
+ in
+ (==), subterms
+ in
+ let with_what =
+ let rec aux = function
+ | 0 -> []
+ | n -> C.Rel 1 :: aux (n-1)
+ in
+ aux (List.length what)
+ in