+let demodulation_all_goal bag env table goal maxnf =
+ let proof,menv,eq,ty,left,right = open_goal goal in
+ let v1, bag, l_demod = demod_all maxnf bag env table ([],menv,left) in
+ let v2, bag, r_demod = demod_all maxnf bag env table ([],menv,right) in
+ let l_demod = if l_demod = [] then [ [], menv, left ] else l_demod in
+ let r_demod = if r_demod = [] then [ [], menv, right ] else r_demod in
+ List.fold_left
+ (fun acc (_,_,l as ld) ->
+ List.fold_left
+ (fun acc (_,_,r as rd) ->
+ combine_demodulation_proofs bag env goal ld rd :: acc)
+ acc r_demod)
+ [] l_demod
+;;