A pseudo-resolution (my terminology) of `M` is a complex `C` such that `∀ i, RⁱF(C) = 0` implies `∀ i, RⁱF(M) = 0`. MacLane's Q' construction has been formalised. Now we need to show that it satisfies the claim above. Depends on #74 and #76
