proposition: Theorem specification_false_like : forall t, t ⊩ 𝔹 0 -> t ★ u·v·π ≻ u ★ π.
proof: Proof. intros t Ht. apply redeq_red. intro Habs. inversion Habs. eelim non_confusion2. eassumption. rewrite <- Hpole. apply Ht. exists (fun n => if eq_nat_dec n 0 then dot π else ⊤). simpl. Ksolve. Ksolve. rewrite Hpole. left. compute in Hπ. now subst. Qed.
imports: Setoid Arith.Peano_dec ClassicalRealizability.Kbase