proposition: Lemma eq_equiv1 : forall T (a a' : T) A e, λ"x" λ"e" "e" @ "x"↓e ⊩ (a = a' ↦ A) → prop (a = a') → A.
proof: Proof. Ksolve. elim (Classical_Prop.classic (a = a')); intro H. left. find. right. find. Qed.
imports: ClassicalRealizability.Kbase