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