proposition: Lemma supterm_nth f : forall n (ts : Tes n) i (hi : i<n), supterm! (apps (Fun f) ts) (Vnth ts hi).
proof: Proof. induction n; intros ts i hi. lia. rewrite (VSn_add ts). rewrite <- app_apps. set (us := Vremove_last ts). set (t0 := Vhead ts). set (tn := Vlast t0 ts). rewrite Vnth_add. destruct (eq_nat_dec i n). subst i. apply t_step. apply st_app_r. trans (apps (Fun f) us). apply t_step. apply st_app_l. apply IHn. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)