proposition: Property red_MyQuote : forall t e π, MyQuote↓e ★ t·π ≻ t ★ Int(Z.of_nat (enumT' t))↓∅·π.
proof: Proof. unfold MyQuote. intros t e π. repeat Kstep. Kred red_kπ₀. repeat Kstep. simpl get. Kred red_quote'. do 5 Kstep. simpl get. apply red_Var. Qed.
imports: ZArith Classical ClassicalRealizability.Kbase ClassicalRealizability.Integers