proposition: Lemma fold_right_length_ts_ge {σ : nat -> poly_type} {ts x} : length ts <= x -> fold_right scons σ ts x = σ (x - length ts).
proof: Proof. move=> ?. have {1}->: x = length ts + (x - length ts) by lia. by rewrite fold_right_length_ts. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun