proposition: Lemma eq_realizer_aux : forall t t' u v π e, eq↓e ★ t·t'·u·v·π ≻(if Z.eq_dec (Z.of_nat (enumP (t·π))) (Z.of_nat (enumP (t'·π))) then u else v) ★ π.
proof: Proof. unfold eq. intros. do 4 Kred red_Lam. Kred red_AppVar. simpl. Kred red_App. Kred red_quote'. do 2 Kred red_Lam. Kred red_AppVar. simpl. Kred red_App. Kred red_quote'. do 2 Kred red_Lam. do 4 Kred red_AppVar. simpl. apply red_ℤeq. Qed.
imports: ZArith Classical ClassicalRealizability.Kbase ClassicalRealizability.Integers