proposition: Lemma prop_term_destruct : forall t F, t ⊩ prop F -> F /\ t ⊩ one \/ ~F /\ t ⊩ ⊤ → ⊥.
proof: Proof. intros t F Ht. elim (Classical_Prop.classic F); intro. left. subtyping. right. split. ok. eapply prop_realizer2'; eassumption. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping