Remove ax-12 from dtru

[CatsAreFluffy]

I added the other non-Tarski axioms of predicate calculus to the $j avoids set as well, since the proof doesn't use those either.

[wlammen]

dtru now depends on a true subset of axioms of those of dtruALT.

[GinoGiotto]

I remember there was a plan to move sn-dtru to main, since it does not require ax-12 nor ax-8 (see comment of bj-dtru).

Ping @benjub @icecream17.

[benjub]

I remember there was a plan to move sn-dtru to main, since it does not require ax-12 nor ax-8 (see comment of bj-dtru).

Ping @benjub @icecream17.

Maybe the easiest way is to merge this MR in order to compare the proofs on the webpages, and then to sort out what we keep as main proof, alt proof, etc., and how we write the various due credits.