proposition: Lemma neq_equiv2 : forall e, λ"x" λ"y" "y" @ "x"↓e ⊩ ∀a a', a ≠ a' → ¬(prop (a = a')).
proof: Proof. Ksolve. unfold prop. destruct (Peano_dec.eq_nat_dec a a'). left. split. ok. find. right. repeat split; ok. Qed.
imports: ClassicalRealizability.Kbase