proposition: Lemma ext_realizer : forall (T : Type) (G : (T -> formula) -> formula) e, ext↓e ⊩ Ext G°.
proof: Proof. unfold Ext, star. repeat Ksolve. Qed.
imports: ZArith Classical ClassicalRealizability.Kbase ClassicalRealizability.Integers