proposition: Lemma fold_right_length_ts_lt {σ: nat -> poly_type} {ts x} : x < length ts -> fold_right scons σ ts x = nth x ts (poly_var 0).
proof: Proof. elim: ts x σ; [ by move=> /=; lia |]. move=> t ts IH [|x] σ /= ?; [done | by apply: IH; lia]. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun