Require Import List.
Import ListNotations.
Inductive formula : Set :=
| var : nat -> formula
| arr : formula -> formula -> formula.
Fixpoint substitute (ζ: nat -> 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 : forall (ζ: nat -> formula) (t: formula), In t Gamma -> hsc Gamma (substitute ζ t)
| hsc_arr : forall (s t : formula), hsc Gamma (arr s t) -> hsc Gamma s -> hsc Gamma t.
Definition HSC_PRV (Gamma: list formula) (s: formula) := hsc Gamma s.
Definition a_b_a : formula := arr (var 0) (arr (var 1) (var 0)).
Definition HSC_AX_PROBLEM := { Gamma: list formula | forall s, In s Gamma -> hsc [a_b_a] s}.
Definition HSC_AX (l: HSC_AX_PROBLEM) := hsc (proj1_sig l) a_b_a.