proposition: Theorem Peano2 : forall e, Id↓e ⊩ ∀(x y : nat), x ≡ y → y ≡ x.
proof: Proof. unfold Leibniz. Kmove. exists (fun n => if eq_nat_dec n x then Z y else Z x). split. destruct (eq_nat_dec x x) as [| Hneq]. ok. now elim Hneq. destruct (eq_nat_dec y x); subst; ok. Qed.
imports: Arith_base ClassicalRealizability.Kbase