proposition: Theorem prop_guard : forall c t t' s, (t ⊩ prop c) -> (c -> t' ★ s ∈ ⫫) -> t ★ t'·s ∈ ⫫.
proof: Proof. intros c t t' s Ht Ht'. elim (Classical_Prop.classic c); intro Hc. apply (prop_realizer1' Hc) in Ht. apply Ht. exists (fun s' => s' = s). split. start. compute in Hπ. subst. now apply Ht'. reflexivity. apply (prop_realizer2' Hc) in Ht. apply Ht. split; ok. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping