proposition: Theorem specification_false_like_easy : forall t, (forall u v π, t ★ u·v·π ≻ u ★ π) -> t ⊩ 𝔹 0.
proof: Proof. intros t Ht. unfold 𝔹. Kmove. eapply anti_evaluation. apply Ht. Kmove. Qed.
imports: Setoid Arith.Peano_dec ClassicalRealizability.Kbase