From Equations Require Import Equations Fin DepElimDec.

Inductive term :=
| Var : nat -> term
| App : term -> list term -> term
| Lam : term -> term.

Equations(nocomp) term_size (t : term) : nat :=
term_size (Var n) := 0;
term_size (App f l) := S (List.fold_left (fun acc x => max acc (term_size x)) l (term_size f));
term_size (Lam f) := S (term_size f).

(** TODO: recognize recursive call under lambda abstraction *)
Equations(nocomp) subst (t : term) (k : nat) (u : term) : term :=
subst t k (Var n) := if Nat.eqb k n then t else Var n;
subst t k (App f l) := App (subst t k f) (List.map (fun x => subst t k x) l);
subst t k (Lam f) := Lam (subst t (S k) f).


