Prove the BD-lemma for MacLane's Q'-construction

[jcommelin]

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