- let bo' = apply_subst subst t in
- let ty = apply_subst subst ty in
- let name = Cic.Name "x" in
- let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ let name = Cic.Name "x" in
+ let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
+ let newgoalproofstep = (rule,pos,id,subst,pred) in