let simplify eq = match eq with
| {f = Implication(x1, y1); g = Implication(x2, y2)} -> {f = x1; g = x2}::[{f = y1; g = y2}]
| {f = Atomic(x); g = Atomic(y)} -> if (x = y) then [] else [eq]
| {f = Implication(x, y); g = Atomic(z)} -> [{f = eq.g; g = eq.f}]
| _ -> [eq]
;;

let solve_impl eqs = List.flatten (List.map simplify eqs);;