+ let id2_ty,l,r =
+ match ty_of id2 seen with
+ | Terms.Node [ _; t; l; r ] ->
+ extract amount vl (Subst.apply_subst subst t),
+ extract amount vl (Subst.apply_subst subst l),
+ extract amount vl (Subst.apply_subst subst r)
+ | _ -> assert false
+ in
+ mk_predicate
+ id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
+ id2_ty,
+ l,r
+ in
+ let l, r, eq_ind =
+ if (ongoal=true) = (dir=Terms.Left2Right) then
+ r,l,eq_ind_r
+ else
+ l,r,eq_ind