- ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
- ~where:where in
- let (selected_context,selected_ty) =
- ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
- let ty' = change context_len ty selected_ty in
+ let where' =
+ ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
+ ~where:where
+ in
+ CicMetaSubst.apply_subst subst where' in
+ let (subst,metasenv,ugraph,selected_context,selected_ty) =
+ ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
+ ~pattern in
+ let ty' = change subst context_len ty selected_ty in