Terms are Well-Founded.

(* PUBLIC DOMAIN *)
Require Export Coq.Vectors.Vector.
Require Export Coq.Lists.List.
Require Import Bool.Bool.
Require Import Logic.FunctionalExtensionality.
Require Import Coq.Program.Wf.

Definition SetVars  := nat.
Definition FuncSymb := nat.
Definition PredSymb := nat.
Record FSV := {
 fs : FuncSymb;
 fsv : nat;
}.
Record PSV := MPSV{
 ps : PredSymb;
 psv : nat;
}.
Inductive Terms : Type :=
| FVC :> SetVars -> Terms
| FSC (f:FSV) : (Vector.t Terms (fsv f)) -> Terms.

Definition rela : forall (x y:Terms), Prop.
Proof.
fix rela 2.
intros x y.
destruct y as [s|f t].
+ exact False.
+ refine (or _ _).
  exact (Vector.In x t).
  simple refine (@Vector.fold_left Terms Prop _ False (fsv f) t).
  intros Q e.
  exact (or Q (rela x e)).
Defined.

Definition snglV {A} (a:A) := Vector.cons A a 0 (Vector.nil A).

Definition wfr : @well_founded Terms rela.
Proof.
clear.
unfold well_founded.
assert (H : forall (n:Terms) (a:Terms), (rela a n) -> Acc rela a).
{ fix iHn 1.
  destruct n.
  + simpl. intros a b; destruct b.
  + simpl. intros a Q. destruct Q as [L|R].
    * admit.  (*apply Acc_intro. intros m Hm. apply (iHn a). exact Hm. *)
    * admit.  (* like in /Arith/Wf_nat.v *)
}
intros a.
simple refine (H _ _ _).
exact (FSC (Build_FSV 0 1) (snglV a)).
simpl.
apply or_introl.
constructor.
Defined.