fact: Fixpoint modus_output_Blist (a1 a2:term) (b : list term) {struct b}: list term := match b with nil => nil term | cons t u => if unify_ok a1 t then cons (modus_output a1 a2 t) (modus_output_Blist a1 a2 u) else (modus_output_Blist a1 a2 u) end.