proposition: Theorem specification_1 : forall t, (t ⊩ one) -> t ★ u·π ≻ u ★ π.
proof: Proof. intros t Ht. apply redeq_red. intro H. inversion H. eelim non_confusion. eassumption. rewrite <- Hpole. apply Ht. exists (dot π). Ksolve. Ksolve. compute in Hπ. subst. rewrite Hpole. now left. Qed.
imports: ClassicalRealizability.Tactics