proposition: Theorem specification_Bool_easy : forall t, (forall u v π, t ★ u·v·π ≻ u ★ π \/ t ★ u·v·π ≻ v ★ π) -> t ⊩ Bool.
proof: Proof. intros t Ht. unfold Bool. Ksolve. destruct (Ht t0 t1 π) as [Hred | Hred]; eapply anti_evaluation; now apply Hred || Ksolve. Qed.
imports: Setoid Arith.Peano_dec ClassicalRealizability.Kbase