Require Export Undecidability.FOL.Arithmetics.FA.
Import Vector.VectorNotations.
Require Import List.
Definition ax_zero_succ := ∀ (zero == σ var 0 → falsity).
Definition ax_succ_inj := ∀∀ (σ $1 == σ $0 → $1 == $0).
Definition ax_cases := ∀ $0 == zero ∨ ∃ $1 == σ $0.
Definition Q := FA ++ (ax_zero_succ::ax_succ_inj::ax_cases::nil).
Definition Qeq :=
EQ ++ Q.
Import Vector.VectorNotations.
Require Import List.
Definition ax_zero_succ := ∀ (zero == σ var 0 → falsity).
Definition ax_succ_inj := ∀∀ (σ $1 == σ $0 → $1 == $0).
Definition ax_cases := ∀ $0 == zero ∨ ∃ $1 == σ $0.
Definition Q := FA ++ (ax_zero_succ::ax_succ_inj::ax_cases::nil).
Definition Qeq :=
EQ ++ Q.