proposition: Lemma eq_equiv2 : forall T (a a' : T) A e, λ"x" "x" @ Id↓e ⊩ (prop (a = a') → A) → a = a' ↦ A.
proof: Proof. Ksolve. start. destruct Hπ as [[] | []]. now apply Id_realizer. contradiction. Qed.
imports: ClassicalRealizability.Kbase