fact: Definition add_to_unifier (t:term) (i:nat) (u:option (table (option term))): option (table (option term)) := let p := nat_pos i in match u with none => none (table (option term)) | some v => match (get p v) with none => some (put (some t) p v) | some r => match (term_ineqL r t) with i_eq => some v | _ => none (table (option term)) end end end.