Require Import List.
Import ListNotations.

Inductive formula : Set :=
  | var : formula
  | arr : formula formula formula.

Fixpoint substitute (ζ: formula) (t: formula) : formula :=
  match t with
  | var n ζ n
  | arr s t arr (substitute ζ s) (substitute ζ t)
  end.

Inductive hsc (Gamma: list formula) : formula Prop :=
  | hsc_var : (ζ: formula) (t: formula), In t hsc (substitute ζ t)
  | hsc_arr : (s t : formula), hsc (arr s t) hsc s hsc t.

Definition HSC_PRV (Gamma: list formula) (s: formula) := hsc s.

Definition a_b_a : formula := arr (var 0) (arr (var 1) (var 0)).

Definition HSC_AX_PROBLEM := { Gamma: list formula | s, In s hsc [a_b_a] s}.

Definition HSC_AX (l: HSC_AX_PROBLEM) := hsc (proj1_sig l) a_b_a.