proposition: Lemma Id_realizer_by_hand : forall e, Id↓e ⊩ one.
proof: Proof. unfold one, Id. intros e π Hπ. destruct Hπ as [Z Hπ]. destruct π as [|t π']. contradiction Hπ. destruct Hπ as [Ht Hπ']. apply anti_evaluation with (t★π'). apply red_trans with ("x"↓("x"←t;e) ★ π'). apply red_Lam. apply red_Var. apply Ht. assumption. Qed.
imports: ClassicalRealizability.Tactics