proposition: Theorem specification_bot_impl_bot_easy : forall t, (forall u π, exists π', t ★ u·π ⪰ u ★ π') -> t ⊩ ⊥ → ⊥.
proof: Proof. intros t Ht. Ksolve. destruct (Ht t0 π) as [π' [Hπ' | Hπ']]. rewrite Hπ'. Kmove. eapply anti_evaluation. apply Hπ'. Kmove. Qed.
imports: ClassicalRealizability.Tactics