proposition: Theorem specification_Bool : forall t, t ⊩ Bool -> t ★ u·v·π ≻ u ★ π \/ t ★ u·v·π ≻ v ★ π.
proof: Proof. intros t Ht. setoid_replace (t ★ u·v·π ≻ u ★ π) with (t ★ u·v·π ⪰ u ★ π). setoid_replace (t ★ u·v·π ≻ v ★ π) with (t ★ u·v·π ⪰ v ★ π). rewrite <- Hpole. apply Ht. exists (dot π). Ksolve. Ksolve. compute in Hπ. subst. rewrite Hpole. now do 2 left. Ksolve. compute in Hπ. subst. rewrite Hpole. now right; left. unfold redeq. intuition. inversion H0. eelim non_confusion2. eassumption. unfold redeq. intuition. inversion H0. eelim non_confusion2. eassumption. Qed.
imports: Setoid Arith.Peano_dec ClassicalRealizability.Kbase