proposition: Lemma stack_prop_iff : forall c t π, t·π ∈ ‖prop c‖ <-> c /\ t★π ∈ ⫫ \/ ~c.
proof: Proof. intros c t π. split; intro Hπ. dec (t·π); try now right. left. split. ok. unfold one in Hπ. dec (t·π). destruct Hπ as [Ht Hπ]. now apply Ht. destruct Hπ as [[Hc Hπ] | Hc]. left. split. ok. exists (fun s => s = π). split. start. compute in Hπ0. now subst. reflexivity. right. repeat split; ok. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping