In view application, close cut formula after substitution

If not, we are creating a capture. The bug is hidden because
we are not using a refreshing substitution in this case.

src/ecHiGoal.ml

@@ -1242,7 +1242,7 @@ let process_view1 pe tc =
             if not (PT.can_concretize pe.PT.ptev_env) then
               tc_error !!tc "cannot infer all placeholders";
 
-            let pt, ax = snd_map (f_forall bds) (PT.concretize pe) in
+            let pt, ax = PT.concretize_gen pe bds in
             t_first (fun subtc ->
               let regen = List.fst regen in
               let ttcut tc =
@@ -1295,9 +1295,9 @@ let process_view1 pe tc =
           if not (PT.can_concretize ptenv) then
             tc_error !!tc "cannot infer all type variables";
 
-          PT.concretize_e_form
+          PT.concretize_e_form_gen
             (PT.concretize_env ptenv)
-            (f_forall (List.map snd ids) cutf)
+            (List.snd ids) cutf
         in
 
         let discharge tc =

src/ecProofTerm.ml

@@ -113,8 +113,14 @@ let concretize_env pe =
   CPTEnv (EcMatching.MEV.assubst pe.pte_ue !(pe.pte_ev) (LDecl.toenv pe.pte_hy))
 
 (* -------------------------------------------------------------------- *)
-let concretize_e_form (CPTEnv subst) f =
-  Fsubst.f_subst subst f
+let concretize_e_form_gen (CPTEnv subst) ids f =
+  let f = Fsubst.f_subst subst f in
+  let ids = List.map (snd_map (Fsubst.subst_gty subst)) ids in
+  f_forall ids f
+
+(* -------------------------------------------------------------------- *)
+let concretize_e_form cptenv f =
+   concretize_e_form_gen cptenv [] f
 
 (* -------------------------------------------------------------------- *)
 let rec concretize_e_arg ((CPTEnv subst) as cptenv) arg =
@@ -141,6 +147,12 @@ and concretize_e_pt cptenv { pt_head; pt_args } =
 let concretize_form pe f =
   concretize_e_form (concretize_env pe) f
 
+(* -------------------------------------------------------------------- *)
+let concretize_gen ({ ptev_env = pe } as pt) ids =
+  let cptenv = concretize_env pe in
+  (concretize_e_pt cptenv pt.ptev_pt,
+   concretize_e_form_gen cptenv ids pt.ptev_ax)
+
 (* -------------------------------------------------------------------- *)
 let concretize ({ ptev_env = pe } as pt) =
   let (CPTEnv subst) as cptenv = concretize_env pe in

src/ecProofTerm.mli

@@ -138,10 +138,12 @@ val pattern_form :
 val can_concretize  : pt_env -> bool
 val concretize_env  : pt_env -> cptenv
 val concretize      : pt_ev  -> proofterm * form
+val concretize_gen  : pt_ev  -> bindings -> proofterm * form
 val concretize_form : pt_env -> form -> form
 
-val concretize_e_form : cptenv -> form -> form
-val concretize_e_arg  : cptenv -> pt_arg -> pt_arg
+val concretize_e_form     : cptenv -> form -> form
+val concretize_e_form_gen : cptenv -> bindings -> form -> form
+val concretize_e_arg      : cptenv -> pt_arg -> pt_arg
 
 (* PTEnv constructor *)
 val ptenv_of_penv : LDecl.hyps -> proofenv -> pt_env

src/ecReduction.ml

@@ -653,8 +653,7 @@ let is_alpha_eq hyps f1 f2 =
     | NotConv -> false
   in
 
-  try aux env EcSubst.empty f1 f2; true
-  with NotConv -> false
+  test env EcSubst.empty f1 f2
 
 (* -------------------------------------------------------------------- *)
 type reduction_info = {