How to prove that terms of a first-order language are well-founded?

Link:: https://stackoverflow.com/q/52087304

Display all goals and responses

Question

Currently, I've started working on proving theorems about first-order logic in Coq (VerifiedMathFoundations). I've proved deduction theorem, but then I got stuck with lemma 1 for theorem of correctness. So I've formulated one elegant piece of the lemma compactly and I invite the community to look at it. That is an incomplete the proof of well-foundness of the terms. How to get rid of the pair of admits properly?

(* 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.Terms -> Terms -> Prop
Proof.Terms -> Terms -> Prop
  fix rela 2.rela: Terms -> Terms -> Prop
Terms -> Terms -> Prop intros x y.rela: Terms -> Terms -> Prop
x, y: Terms
Prop destruct y as [s|f t].rela: Terms -> Terms -> Prop
x: Terms
s: SetVars
Prop
rela: Terms -> Terms -> Prop
x: Terms
f: FSV
t: Vector.t Terms (fsv f)
Prop
  -rela: Terms -> Terms -> Prop
x: Terms
s: SetVars
Prop exact False.
  -rela: Terms -> Terms -> Prop
x: Terms
f: FSV
t: Vector.t Terms (fsv f)
Prop refine (or _ _).rela: Terms -> Terms -> Prop
x: Terms
f: FSV
t: Vector.t Terms (fsv f)
Prop
rela: Terms -> Terms -> Prop
x: Terms
f: FSV
t: Vector.t Terms (fsv f)
Prop
    exact (Vector.In x t).rela: Terms -> Terms -> Prop
x: Terms
f: FSV
t: Vector.t Terms (fsv f)
Prop
    simple refine (@Vector.fold_left Terms Prop _ False (fsv f) t).rela: Terms -> Terms -> Prop
x: Terms
f: FSV
t: Vector.t Terms (fsv f)
Prop -> Terms -> Prop
    intros Q e.rela: Terms -> Terms -> Prop
x: Terms
f: FSV
t: Vector.t Terms (fsv f)
Q: Prop
e: Terms
Prop
    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.well_founded rela
Proof.well_founded rela
  clear.well_founded rela unfold well_founded.forall a : Terms, Acc rela a
  assert (H : forall (n:Terms) (a:Terms), (rela a n) -> Acc rela a).forall n a : Terms, rela a n -> Acc rela a
H: forall n a : Terms, rela a n -> Acc rela a
forall a : Terms, Acc rela a
  {forall n a : Terms, rela a n -> Acc rela a fix iHn 1.iHn: forall n a : Terms, rela a n -> Acc rela a
forall n a : Terms, rela a n -> Acc rela a destruct n.iHn: forall n a : Terms, rela a n -> Acc rela a
s: SetVars
forall a : Terms, rela a s -> Acc rela a
iHn: forall n a : Terms, rela a n -> Acc rela a
f: FSV
t: Vector.t Terms (fsv f)
forall a : Terms, rela a (FSC f t) -> Acc rela a
    -iHn: forall n a : Terms, rela a n -> Acc rela a
s: SetVars
forall a : Terms, rela a s -> Acc rela a simpl.iHn: forall n a : Terms, rela a n -> Acc rela a
s: SetVars
forall a : Terms, False -> Acc rela a intros a b.iHn: forall n a : Terms, rela a n -> Acc rela a
s: SetVars
a: Terms
b: False
Acc rela a destruct b.
    -iHn: forall n a : Terms, rela a n -> Acc rela a
f: FSV
t: Vector.t Terms (fsv f)
forall a : Terms, rela a (FSC f t) -> Acc rela a simpl.iHn: forall n a : Terms, rela a n -> Acc rela a
f: FSV
t: Vector.t Terms (fsv f)
forall a : Terms,
Vector.In a t \/
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela a e) False
  t -> Acc rela a intros a Q.iHn: forall n a : Terms, rela a n -> Acc rela a
f: FSV
t: Vector.t Terms (fsv f)
a: Terms
Q: Vector.In a t \/
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela a e)
  False t
Acc rela a destruct Q as [L|R].iHn: forall n a : Terms, rela a n -> Acc rela a
f: FSV
t: Vector.t Terms (fsv f)
a: Terms
L: Vector.In a t
Acc rela a
iHn: forall n a : Terms, rela a n -> Acc rela a
f: FSV
t: Vector.t Terms (fsv f)
a: Terms
R: Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela a e)
  False t
Acc rela a
      +iHn: forall n a : Terms, rela a n -> Acc rela a
f: FSV
t: Vector.t Terms (fsv f)
a: Terms
L: Vector.In a t
Acc rela a admit.
        (* smth like apply Acc_intro. intros m Hm. apply (iHn a). exact Hm. *)
      +iHn: forall n a : Terms, rela a n -> Acc rela a
f: FSV
t: Vector.t Terms (fsv f)
a: Terms
R: Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela a e)
  False t
Acc rela a admit.
        (* like in /Arith/Wf_nat.v *)
  }H: forall n a : Terms, rela a n -> Acc rela a
forall a : Terms, Acc rela a
  intros a.H: forall n a : Terms, rela a n -> Acc rela a
a: Terms
Acc rela a simple refine (H _ _ _).H: forall n a : Terms, rela a n -> Acc rela a
a: Terms
Terms
H: forall n a : Terms, rela a n -> Acc rela a
a: Terms
rela a ?n
  exact (FSC (Build_FSV 0 1) (snglV a)).H: forall n a : Terms, rela a n -> Acc rela a
a: Terms
rela a (FSC {| fs := 0; fsv := 1 |} (snglV a))
  simpl.H: forall n a : Terms, rela a n -> Acc rela a
a: Terms
Vector.In a (snglV a) \/ False \/ rela a a apply or_introl.H: forall n a : Terms, rela a n -> Acc rela a
a: Terms
Vector.In a (snglV a) constructor.
Defined.(in proof wfr): Attempt to save a proof with given up
goals. If this is really what you want to do, use
Admitted in place of Qed.

It is also available here: pastebin.

Update: At least transitivity is needed for well-foundness. I also started a proof, but didn't finished.

Fixpoint Tra (a b c : Terms) (Hc : rela c b) (Hb : rela b a) {struct a} :
  rela c a.Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
a, b, c: Terms
Hc: rela c b
Hb: rela b a
rela c a
Proof.Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
a, b, c: Terms
Hc: rela c b
Hb: rela b a
rela c a
  destruct a.Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
s: SetVars
b, c: Terms
Hc: rela c b
Hb: rela b s
rela c s
Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
f: FSV
t: Vector.t Terms (fsv f)
b, c: Terms
Hc: rela c b
Hb: rela b (FSC f t)
rela c (FSC f t)
  -Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
s: SetVars
b, c: Terms
Hc: rela c b
Hb: rela b s
rela c s simpl in * |- *.Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
s: SetVars
b, c: Terms
Hc: rela c b
Hb: False
False exact Hb.
  -Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
f: FSV
t: Vector.t Terms (fsv f)
b, c: Terms
Hc: rela c b
Hb: rela b (FSC f t)
rela c (FSC f t) simpl in * |- *.Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
f: FSV
t: Vector.t Terms (fsv f)
b, c: Terms
Hc: rela c b
Hb: Vector.In b t \/
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela b e)
  False t
Vector.In c t \/
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela c e) False
  t destruct Hb.Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
f: FSV
t: Vector.t Terms (fsv f)
b, c: Terms
Hc: rela c b
H: Vector.In b t
Vector.In c t \/
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela c e) False
  t
Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
f: FSV
t: Vector.t Terms (fsv f)
b, c: Terms
Hc: rela c b
H: Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela b e)
  False t
Vector.In c t \/
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela c e) False
  t
    +Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
f: FSV
t: Vector.t Terms (fsv f)
b, c: Terms
Hc: rela c b
H: Vector.In b t
Vector.In c t \/
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela c e) False
  t apply or_intror.Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
f: FSV
t: Vector.t Terms (fsv f)
b, c: Terms
Hc: rela c b
H: Vector.In b t
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela c e) False
  t revert f t H .Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
b, c: Terms
Hc: rela c b
forall (f : FSV) (t : t Terms (fsv f)),
Vector.In b t ->
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela c e) False
  t fix RECU 1.Tra: forall a b c : Terms, rela c b -> rela b a -> rela c a
b, c: Terms
Hc: rela c b
RECU: forall (f : FSV) (t : t Terms (fsv f)),
Vector.In b t ->
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela c e)
  False t
forall (f : FSV) (t : t Terms (fsv f)),
Vector.In b t ->
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela c e) False
  t intros f t H.Tra: forall a b c : Terms,
rela c b -> rela b a -> rela c a
b, c: Terms
Hc: rela c b
RECU: forall (f : FSV) (t : Vector.t Terms (fsv f)),
Vector.In b t ->
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela c e)
  False t
f: FSV
t: Vector.t Terms (fsv f)
H: Vector.In b t
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela c e) False
  t
    (* ... *)
Admitted.

Answer

You can do it by defining a height function on Terms, and showing that decreasing rela implies decreasing heights:

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;
    }.

Unset Elimination Schemes.
Inductive Terms : Type :=
| FVC :> SetVars -> Terms
| FSC (f : FSV) : Vector.t Terms (fsv f) -> Terms.
Set Elimination Schemes.

Definition Terms_rect (T : Terms -> Type)
           (H_FVC : forall sv, T (FVC sv))
           (H_FSC : forall f v,
               (forall n, T (Vector.nth v n)) -> T (FSC f v)) :=
  fix loopt (t : Terms) : T t :=
    match t with
    | FVC sv  => H_FVC sv
    | FSC f v =>
      let fix loopv s (v : Vector.t Terms s) : forall n, T (Vector.nth v n) :=
          match v with
          | @Vector.nil _ => Fin.case0 _
          | @Vector.cons _ t _ v =>
            fun n =>
              Fin.caseS' n (fun n => T (Vector.nth (Vector.cons _ t _ v) n))
                         (loopt t)
                         (loopv _ v)
          end in
      H_FSC f v (loopv _ v)
    end.

Definition Terms_ind := Terms_rect.

Fixpoint height (t : Terms) : nat :=
  match t with
  | FVC _ => 0
  | FSC f v => S (Vector.fold_right (fun t acc => Nat.max acc (height t)) v 0)
  end.

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

Require Import Lia.

Definition wfr : @well_founded Terms rela.well_founded rela
Proof.well_founded rela
  apply (Wf_nat.well_founded_lt_compat _ height).forall x y : Terms, rela x y -> height x < height y
  intros t1 t2.t1, t2: Terms
rela t1 t2 -> height t1 < height t2 induction t2 as [sv2|f2 v2 IH]; simpl; try easy.t1: Terms
f2: FSV
v2: t Terms (fsv f2)
IH: forall n : Fin.t (fsv f2),
rela t1 (Vector.nth v2 n) ->
height t1 < height (Vector.nth v2 n)
Vector.In t1 v2 \/
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela t1 e) False
  v2 ->
height t1 <
S
  (Vector.fold_right
     (fun (t : Terms) (acc : nat) =>
      Nat.max acc (height t)) v2 0)
  intros [t_v|t_sub]; apply Lt.le_lt_n_Sm.t1: Terms
f2: FSV
v2: t Terms (fsv f2)
IH: forall n : Fin.t (fsv f2),
rela t1 (Vector.nth v2 n) ->
height t1 < height (Vector.nth v2 n)
t_v: Vector.In t1 v2
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
t1: Terms
f2: FSV
v2: t Terms (fsv f2)
IH: forall n : Fin.t (fsv f2),
rela t1 (Vector.nth v2 n) ->
height t1 < height (Vector.nth v2 n)
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
  {t1: Terms
f2: FSV
v2: t Terms (fsv f2)
IH: forall n : Fin.t (fsv f2),
rela t1 (Vector.nth v2 n) ->
height t1 < height (Vector.nth v2 n)
t_v: Vector.In t1 v2
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0 clear IH.t1: Terms
f2: FSV
v2: t Terms (fsv f2)
t_v: Vector.In t1 v2
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0 induction t_v; simpl; lia. }t1: Terms
f2: FSV
v2: t Terms (fsv f2)
IH: forall n : Fin.t (fsv f2),
rela t1 (Vector.nth v2 n) ->
height t1 < height (Vector.nth v2 n)
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
  revert v2 IH t_sub.t1: Terms
f2: FSV
forall v2 : t Terms (fsv f2),
(forall n : Fin.t (fsv f2),
 rela t1 (Vector.nth v2 n) ->
 height t1 < height (Vector.nth v2 n)) ->
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela t1 e) False
  v2 ->
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0 generalize (fsv f2).t1: Terms
f2: FSV
forall (n : nat) (v2 : t Terms n),
(forall n0 : Fin.t n,
 rela t1 (Vector.nth v2 n0) ->
 height t1 < height (Vector.nth v2 n0)) ->
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela t1 e) False
  v2 ->
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0 clear f2.t1: Terms
forall (n : nat) (v2 : t Terms n),
(forall n0 : Fin.t n,
 rela t1 (Vector.nth v2 n0) ->
 height t1 < height (Vector.nth v2 n0)) ->
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela t1 e) False
  v2 ->
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
  intros k v2 IH t_sub.t1: Terms
k: nat
v2: t Terms k
IH: forall n : Fin.t k,
rela t1 (Vector.nth v2 n) ->
height t1 < height (Vector.nth v2 n)
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
  enough (H : exists n, rela t1 (Vector.nth v2 n)).t1: Terms
k: nat
v2: t Terms k
IH: forall n : Fin.t k,
rela t1 (Vector.nth v2 n) ->
height t1 < height (Vector.nth v2 n)
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
H: exists n : Fin.t k, rela t1 (Vector.nth v2 n)
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
t1: Terms
k: nat
v2: t Terms k
IH: forall n : Fin.t k,
rela t1 (Vector.nth v2 n) ->
height t1 < height (Vector.nth v2 n)
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
  {t1: Terms
k: nat
v2: t Terms k
IH: forall n : Fin.t k,
rela t1 (Vector.nth v2 n) ->
height t1 < height (Vector.nth v2 n)
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
H: exists n : Fin.t k, rela t1 (Vector.nth v2 n)
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0 destruct H as [n H].t1: Terms
k: nat
v2: t Terms k
IH: forall n : Fin.t k,
rela t1 (Vector.nth v2 n) ->
height t1 < height (Vector.nth v2 n)
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
n: Fin.t k
H: rela t1 (Vector.nth v2 n)
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0 apply IH in H.t1: Terms
k: nat
v2: t Terms k
IH: forall n : Fin.t k,
rela t1 (Vector.nth v2 n) ->
height t1 < height (Vector.nth v2 n)
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
n: Fin.t k
H: height t1 < height (Vector.nth v2 n)
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0 clear IH t_sub.t1: Terms
k: nat
v2: t Terms k
n: Fin.t k
H: height t1 < height (Vector.nth v2 n)
height t1 <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
    transitivity (height (Vector.nth v2 n)); try lia; clear H.t1: Terms
k: nat
v2: t Terms k
n: Fin.t k
height (Vector.nth v2 n) <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
    induction v2 as [|t2 m v2 IHv2].t1: Terms
n: Fin.t 0
height (Vector.nth (Vector.nil Terms) n) <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) 
  (Vector.nil Terms) 0
t1, t2: Terms
m: nat
v2: t Terms m
n: Fin.t (S m)
IHv2: forall n : Fin.t m,
height (Vector.nth v2 n) <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
height (Vector.nth (Vector.cons Terms t2 m v2) n) <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) 
  (Vector.cons Terms t2 m v2) 0
    -t1: Terms
n: Fin.t 0
height (Vector.nth (Vector.nil Terms) n) <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) 
  (Vector.nil Terms) 0 inversion n.
    -t1, t2: Terms
m: nat
v2: t Terms m
n: Fin.t (S m)
IHv2: forall n : Fin.t m,
height (Vector.nth v2 n) <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
height (Vector.nth (Vector.cons Terms t2 m v2) n) <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) 
  (Vector.cons Terms t2 m v2) 0 apply (Fin.caseS' n); clear n; simpl; try lia.t1, t2: Terms
m: nat
v2: t Terms m
IHv2: forall n : Fin.t m,
height (Vector.nth v2 n) <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
forall p : Fin.t m,
height (Vector.nth v2 p) <=
Nat.max
  (Vector.fold_right
     (fun (t : Terms) (acc : nat) =>
      Nat.max acc (height t)) v2 0) 
  (height t2)
      intros n.t1, t2: Terms
m: nat
v2: t Terms m
IHv2: forall n : Fin.t m,
height (Vector.nth v2 n) <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
n: Fin.t m
height (Vector.nth v2 n) <=
Nat.max
  (Vector.fold_right
     (fun (t : Terms) (acc : nat) =>
      Nat.max acc (height t)) v2 0) 
  (height t2) specialize (IHv2 n).t1, t2: Terms
m: nat
v2: t Terms m
n: Fin.t m
IHv2: height (Vector.nth v2 n) <=
Vector.fold_right
  (fun (t : Terms) (acc : nat) =>
   Nat.max acc (height t)) v2 0
height (Vector.nth v2 n) <=
Nat.max
  (Vector.fold_right
     (fun (t : Terms) (acc : nat) =>
      Nat.max acc (height t)) v2 0) 
  (height t2) lia. }t1: Terms
k: nat
v2: t Terms k
IH: forall n : Fin.t k,
rela t1 (Vector.nth v2 n) ->
height t1 < height (Vector.nth v2 n)
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
  clear IH.t1: Terms
k: nat
v2: t Terms k
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
  assert (H : Vector.fold_right (fun t Q => Q \/ rela t1 t) v2 False).t1: Terms
k: nat
v2: t Terms k
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t) v2
  False
t1: Terms
k: nat
v2: t Terms k
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
H: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
  {t1: Terms
k: nat
v2: t Terms k
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t) v2
  False revert t_sub.t1: Terms
k: nat
v2: t Terms k
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela t1 e) False
  v2 ->
Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t) v2
  False generalize False.t1: Terms
k: nat
v2: t Terms k
forall P : Prop,
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela t1 e) P v2 ->
Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t) v2 P
    induction v2 as [|t2 n v2]; simpl in *; trivial.t1, t2: Terms
n: nat
v2: t Terms n
IHv2: forall P : Prop,
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela t1 e)
  P v2 ->
Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 P
forall P : Prop,
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela t1 e)
  (P \/ rela t1 t2) v2 ->
Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t) v2 P \/
rela t1 t2
    intros P H.t1, t2: Terms
n: nat
v2: t Terms n
IHv2: forall P : Prop,
Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela t1 e)
  P v2 ->
Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 P
P: Prop
H: Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela t1 e)
  (P \/ rela t1 t2) v2
Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t) v2 P \/
rela t1 t2 specialize (IHv2 _ H).t1, t2: Terms
n: nat
v2: t Terms n
P: Prop
IHv2: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 (P \/ rela t1 t2)
H: Vector.fold_left
  (fun (Q : Prop) (e : Terms) => Q \/ rela t1 e)
  (P \/ rela t1 t2) v2
Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t) v2 P \/
rela t1 t2 clear H.t1, t2: Terms
n: nat
v2: t Terms n
P: Prop
IHv2: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 (P \/ rela t1 t2)
Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t) v2 P \/
rela t1 t2
    induction v2 as [|t2' n v2 IHv2']; simpl in *; tauto. }t1: Terms
k: nat
v2: t Terms k
t_sub: Vector.fold_left
  (fun (Q : Prop) (e : Terms) =>
   Q \/ rela t1 e) False v2
H: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
  clear t_sub.t1: Terms
k: nat
v2: t Terms k
H: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
  induction v2 as [|t2 k v2 IH]; simpl in *; try easy.t1, t2: Terms
k: nat
v2: t Terms k
H: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False \/ rela t1 t2
IH: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False ->
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
exists n : Fin.t (S k),
  rela t1
    (match
       n in (Fin.t m') return (t Terms m' -> Terms)
     with
     | @Fin.F1 n0 =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Terms)
           (fun (h : Terms) 
              (n1 : nat) 
              (_ : t Terms n1) => h)
     | @Fin.FS n0 p' =>
         fun v : t Terms (S n0) =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Fin.t n1 -> Terms)
           (fun (_ : Terms) 
              (n1 : nat) 
              (t : t Terms n1) 
              (p0 : Fin.t n1) => 
            Vector.nth t p0) v p'
     end (Vector.cons Terms t2 k v2))
  destruct H as [H|H].t1, t2: Terms
k: nat
v2: t Terms k
H: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False
IH: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False ->
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
exists n : Fin.t (S k),
  rela t1
    (match
       n in (Fin.t m') return (t Terms m' -> Terms)
     with
     | @Fin.F1 n0 =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Terms)
           (fun (h : Terms) 
              (n1 : nat) 
              (_ : t Terms n1) => h)
     | @Fin.FS n0 p' =>
         fun v : t Terms (S n0) =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Fin.t n1 -> Terms)
           (fun (_ : Terms) 
              (n1 : nat) 
              (t : t Terms n1) 
              (p0 : Fin.t n1) => 
            Vector.nth t p0) v p'
     end (Vector.cons Terms t2 k v2))
t1, t2: Terms
k: nat
v2: t Terms k
H: rela t1 t2
IH: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False ->
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
exists n : Fin.t (S k),
  rela t1
    (match
       n in (Fin.t m') return (t Terms m' -> Terms)
     with
     | @Fin.F1 n0 =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Terms)
           (fun (h : Terms) 
              (n1 : nat) 
              (_ : t Terms n1) => h)
     | @Fin.FS n0 p' =>
         fun v : t Terms (S n0) =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Fin.t n1 -> Terms)
           (fun (_ : Terms) 
              (n1 : nat) 
              (t : t Terms n1) 
              (p0 : Fin.t n1) => 
            Vector.nth t p0) v p'
     end (Vector.cons Terms t2 k v2))
  -t1, t2: Terms
k: nat
v2: t Terms k
H: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False
IH: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False ->
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
exists n : Fin.t (S k),
  rela t1
    (match
       n in (Fin.t m') return (t Terms m' -> Terms)
     with
     | @Fin.F1 n0 =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Terms)
           (fun (h : Terms) 
              (n1 : nat) 
              (_ : t Terms n1) => h)
     | @Fin.FS n0 p' =>
         fun v : t Terms (S n0) =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Fin.t n1 -> Terms)
           (fun (_ : Terms) 
              (n1 : nat) 
              (t : t Terms n1) 
              (p0 : Fin.t n1) => 
            Vector.nth t p0) v p'
     end (Vector.cons Terms t2 k v2)) apply IH in H.t1, t2: Terms
k: nat
v2: t Terms k
H: exists n : Fin.t k, rela t1 (Vector.nth v2 n)
IH: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False ->
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
exists n : Fin.t (S k),
  rela t1
    (match
       n in (Fin.t m') return (t Terms m' -> Terms)
     with
     | @Fin.F1 n0 =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Terms)
           (fun (h : Terms) 
              (n1 : nat) 
              (_ : t Terms n1) => h)
     | @Fin.FS n0 p' =>
         fun v : t Terms (S n0) =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Fin.t n1 -> Terms)
           (fun (_ : Terms) 
              (n1 : nat) 
              (t : t Terms n1) 
              (p0 : Fin.t n1) => 
            Vector.nth t p0) v p'
     end (Vector.cons Terms t2 k v2)) destruct H as [n Hn].t1, t2: Terms
k: nat
v2: t Terms k
n: Fin.t k
Hn: rela t1 (Vector.nth v2 n)
IH: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False ->
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
exists n : Fin.t (S k),
  rela t1
    (match
       n in (Fin.t m') return (t Terms m' -> Terms)
     with
     | @Fin.F1 n0 =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Terms)
           (fun (h : Terms) 
              (n1 : nat) 
              (_ : t Terms n1) => h)
     | @Fin.FS n0 p' =>
         fun v : t Terms (S n0) =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Fin.t n1 -> Terms)
           (fun (_ : Terms) 
              (n1 : nat) 
              (t : t Terms n1) 
              (p0 : Fin.t n1) => 
            Vector.nth t p0) v p'
     end (Vector.cons Terms t2 k v2)) now (exists (Fin.FS n)).
  -t1, t2: Terms
k: nat
v2: t Terms k
H: rela t1 t2
IH: Vector.fold_right
  (fun (t : Terms) (Q : Prop) => Q \/ rela t1 t)
  v2 False ->
exists n : Fin.t k, rela t1 (Vector.nth v2 n)
exists n : Fin.t (S k),
  rela t1
    (match
       n in (Fin.t m') return (t Terms m' -> Terms)
     with
     | @Fin.F1 n0 =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Terms)
           (fun (h : Terms) 
              (n1 : nat) 
              (_ : t Terms n1) => h)
     | @Fin.FS n0 p' =>
         fun v : t Terms (S n0) =>
         caseS
           (fun (n1 : nat) (_ : t Terms (S n1)) =>
            Fin.t n1 -> Terms)
           (fun (_ : Terms) 
              (n1 : nat) 
              (t : t Terms n1) 
              (p0 : Fin.t n1) => 
            Vector.nth t p0) v p'
     end (Vector.cons Terms t2 k v2)) now exists Fin.F1.
Qed.

(Note the use of the custom induction principle, which is needed because of the nested inductives.)

This style of development, however, is too complicated. Avoiding certain pitfalls would greatly simplify it:

The Coq standard vector library is too hard to use. The issue here is exacerbated because of the nested inductives. It would probably be better to use plain lists and have a separate well-formedness predicate on terms.

Defining a relation such as rela in proof mode makes it harder to read. Consider, for instance, the following simpler alternative:

Fixpoint rela x y :=
  match y with
  | FVC _ => False
  | FSC f v =>
    Vector.In x v \/
    Vector.fold_right (fun z P => rela x z \/ P) v False
  end.

Folding left has a poor reduction behavior, because it forces us to generalize over the accumulator argument to get the induction to go through. This is why in my proof I had to switch to a fold_right.