Theorem aprilfools2025

Description: An abuse of notation. (Contributed by Prof. Loof Lirpa, 1-Apr-2025) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	aprilfools2025	$$⊢\left\{⟨“April”⟩,⟨“fools!”⟩\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		s4cli	$$⊢⟨“⟨“⟨“Never”⟩⟨“gonna”⟩⟨“give”⟩⟨“you”⟩⟨“up”⟩”⟩⟨“⟨“Never”⟩⟨“gonna”⟩⟨“let”⟩⟨“you”⟩⟨“down”⟩”⟩⟨“⟨“Never”⟩⟨“gonna”⟩⟨“turn”⟩⟨“around”⟩⟨“and”⟩”⟩⟨“⟨“desert”⟩⟨“you!”⟩”⟩”⟩\in \mathrm{Word}\mathrm{V}$$
2		prex	$$⊢\left\{⟨“April”⟩,⟨“fools!”⟩\right\}\in \mathrm{V}$$
3	1 2	iddii	$$⊢\left\{⟨“April”⟩,⟨“fools!”⟩\right\}\in \mathrm{V}$$