proposition: Theorem eq_realizer1 : forall t t' u v π e, t = t' -> eq↓e ★ t·t'·u·v·π ≻ u ★ π.
proof: Proof. intros. subst t'. replace (u ★ π) with ((if Z.eq_dec (Z.of_nat (enumP (t·π))) (Z.of_nat (enumP (t·π))) then u else v) ★ π). now apply eq_realizer_aux. destruct (Z.eq_dec _ _) as [? | Hneq]. reflexivity. now elim Hneq. Qed.
imports: ZArith Classical ClassicalRealizability.Kbase ClassicalRealizability.Integers