[R.reduce ~delta:true ~subst context (0,[],[],t1,[]),
R.reduce ~delta:true ~subst context (0,[],[],t2,[])]
(*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*)
[R.reduce ~delta:true ~subst context (0,[],[],t1,[]),
R.reduce ~delta:true ~subst context (0,[],[],t2,[])]
(*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*)