proposition: Theorem guard : forall c F t t' e, (t↓e ⊩ prop c) -> (t'↓e ⊩ F) -> (t @ t')↓e ⊩ (c ↦ F).
proof: Proof. intros c F t t' e Ht Ht'. start. apply Ht. left. split. ok. exists F. split. ok. now apply Hπ. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping