Starting theory proving mode: "No matching clauses for match."

[ruplet]

Hey!

I'm trying to define a weak arithmetical theory with some basic axioms and one axiom scheme: induction for formulas with bounded quantifiers only (quantifier is bounded if it's of the form: Exists x, x <= t \and phi or Forall x, x <= t -> phi. formula is bounded if every quantifier is bounded). I can successfully:
a) start non-theory proof mode and finish a proof of (∀$0 == $0) in it
b) define my theory IOPENeq, including induction axiom scheme
c) start proof mode of Coq for the theorem I need to prove: Lemma add_assoc : Delta0eq ⊢T ∀∀∀ ((($0 ⊕ $1) ⊕ $2) == ($0 ⊕ ($1 ⊕ $2))).

and then when applying fstart, I get an error like this:

I attach my (non-minimal, but I guess small enough) non-working example:

From FOL Require Import ArithmeticalHierarchySyntactic.
From FOL Require Import FullSyntax Arithmetics.
Import FOL.PA.
Require Import List.
From FOL.Proofmode Require Import Theories ProofMode.

Existing Instance PA_preds_signature.
Existing Instance PA_funcs_signature.

Check ax_add_zero.

Section WithPeirce.
(* Existing Instance peirce_classical. *)

Context {peirce : peirce}.

(* ctrl + shift + u 22a2 enter *)
(* forall: 2200 *)
Lemma refl_eq : Qeq ⊢ ∀$0 == $0.
Proof.
  fstart.
  fintros.
  fapply ax_refl.
Qed.

Existing Instance falsity_on.

(* Warning: `t` cannot contain occurences of 'x' ($0),
but I don't know how to enforce it. *)  
Inductive delta0_ind : form -> Prop :=
| d0_false : delta0_ind falsity
| d0_atom P v : delta0_ind ((atom P v): form)
| d0_bin op (phi1 phi2: form) :
    delta0_ind phi1 ->
    delta0_ind phi2 ->
    delta0_ind (bin op phi1 phi2)
| d0_bdEx t (phi1: form) :
    delta0_ind phi1 ->
    delta0_ind (∃ ($0 ⧀= t ∧ phi1))
| d0_bdAll t (phi1 : form):
    delta0_ind phi1 ->
    delta0_ind (∀ ($0 ⧀= t → phi1)).

Check delta0_ind.
Check ax_induction.

Definition one := σ zero.
(* B1. x + 1 ≠ 0 *)
Definition B1 : form := ∀ ¬ ( ($0 ⊕ one) == zero ).

(* B2. x + 1 = y + 1 → x = y *)
Definition B2 : form := ∀∀ ( ($1 ⊕ one) == ($0 ⊕ one) → $1 == $0 ).

(* B3. x + 0 = x *)
Definition B3 : form := ∀ ( $0 ⊕ zero == $0 ).

(* B4. x + (y + 1) = (x + y) + 1   ≡   x ⊕ σ y = σ (x ⊕ y) *)
Definition B4 : form := ∀∀ ( $1 ⊕ σ $0 == σ ($1 ⊕ $0) ).

(* B5. x · 0 = 0 *)
Definition B5 : form := ∀ ( $0 ⊗ zero == zero ).

(* B6. x · (y + 1) = (x · y) + x *)
Definition B6 : form := ∀∀ ( $1 ⊗ ( $0 ⊕ one ) == ( $1 ⊗ $0 ) ⊕ $1 ).

(* B7. (x ≤ y ∧ y ≤ x) → x = y *)
(* uses the library’s ≤ notation ⧀= *)
Definition B7 : form := ∀∀ ( ( $1 ⧀= $0 ∧ $0 ⧀= $1 ) → $1 == $0 ).

(* B8. x ≤ x + y *)
Definition B8 : form := ∀∀ ( $0 ⧀= ( $0 ⊕ $1 ) ).

(* C. 0 + 1 = 1 *)
Definition C  : form := ( zero ⊕ one == one ).
Definition Beq_axioms : list form := B1 :: B2 :: B3 :: B4 :: B5 :: B6 :: B7 :: B8 :: C :: EQ.


Inductive Delta0eq : form -> Prop :=
  ax_B phi : In phi Beq_axioms -> Delta0eq phi
| ind phi : delta0_ind phi -> Delta0eq (ax_induction phi).

Lemma add_assoc : Delta0eq ⊢T ∀∀∀ ((($0 ⊕ $1) ⊕ $2) == ($0 ⊕ ($1 ⊕ $2))).
Proof.
  fstart.
  make_compatible fstart.
  fstart.
  fintro.

I'll appreciate your help on pinpointing where's the problem with fstart failing to start theory-proof mode!

Thanks :)
ruplet

Update:
using ⊩ instead of ⊢T allows me to execute fstart, but fintro / fintros don't make progress afterwards anyway

Update2:
After using ⊩ and doing an fstart, I was able to try apply TAllI, which gave me this informative error message:

and indeed, the goal hidden behind the library's syntax is of the form "exists list A such that A is in the theory IDelta0, and from A we can prove phi", not of the form "forall x, y, z, phi(x, y, z)". Probably that's the core issue. link to def of TAllI