proposition: Theorem Peano3 : forall e, Id↓e ⊩ ∀(x y z : nat), x ≡ y → y ≡ z → x ≡ z.
proof: Proof. unfold Leibniz at 1. Kmove. exists (fun n => if eq_nat_dec n x then y ≡ z else x ≡ z). 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