proposition: Theorem guard_sub : forall c F e π , π ∈ ‖c ↦ F‖ -> Id↓e·π ∈ ‖prop c → F‖.
proof: Proof. intros c F e π Hπ. destruct Hπ as [Hc Hπ]. split; try ok. now apply prop_realizer1. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping