proposition: Theorem Impl_eta_realizer : forall A B t e, (forall t' e, t'↓e ⊩ A -> t @ t'↓e ⊩ B) -> (λ"x" t @ "x")↓e ⊩ A → B.
proof: Proof. intros A B t e Ht. startn 1. apply (Ht "x"); Ksolve. Qed.
imports: ClassicalRealizability.Tactics