Add more stacked tilde variants

[MDLC01]

This adds a few symbols composed of stacked tildes and horizontal lines. I explain the reasoning for each change below.

• tilde.double makes sense in my opinion as a non-semantic variant of approx. I have chosen to only include the .not variant but I am open to including .eq, .equiv, and .hat as well. I am also open to excluding tilde.double from this PR if we are unable to reach a consensus.

• The rename from minus.tilde to eq.tilde is consistent with the existing tilde.eq, as well as the Unicode character being a Relation, not a Binary, even though its name uses "MINUS" instead of "EQUAL". Same for tilde.eq.tilde.

• equiv.tilde is consistent with the existing tilde.equiv.

• approx.equiv is consistent with other uses of .equiv, such as in tilde.equiv.

[MDLC01]

This PR is missing three approvals to be merged. If you disagree with a specific change, feel free to express your concern here or on Discord.

[T0mstone]

I think eq.tilde and equiv.tilde are good.

tilde.tilde is problematic because tilde.eq.tilde is equivalent to tilde.tilde.eq, so I would be against both of these.

And in the abscence of tilde.tilde and tilde.tilde.eq, I'm also on board with approx.equiv.

[MDLC01]

tilde.tilde is problematic

I don't understand what you mean: tilde.tilde does not exist as a variant right now, although it is accepted and falls back to tilde.eq.tilde.

[T0mstone]

I mean that tilde.tilde.eq would be the actual problem, since you'd expect that to be ≊, but it's actually equivalent to tilde.eq.tilde, which would be ⩬.

And I take this as reason enough to throw out tilde.tilde altogether, tho now that I think about it there might be a case for having just tilde.tilde with no other modifiers.

[MDLC01]

If you means that tilde.tilde should be a name for ≈, I believe tilde.double would be a more appropriate name.

[T0mstone]

Oh, right, there's that as well. Even worse then, since adding tilde.eq.tilde would add tilde.tilde as fallback for it, so then you don't even get an error if you misremember tilde.double as tilde.tilde.