- NCic.LetIn ("clause_" ^ string_of_int id,
- close_with_forall vl (extract amount vl lit),
+ let body = aux ongoal
+ ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl
+ in
+ if NCicUntrusted.count_occurrences [] 0 body <= 1 then
+ NCicSubstitution.subst
+ ~avoid_beta_redexes:true ~no_implicit:false
+ (close_with_lambdas vl (NCic.Appl
+ [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]))
+ body
+ else
+ NCic.LetIn ("clause_" ^ string_of_int id,
+ close_with_forall vl (extract amount vl lit),