proposition: Lemma iter_scons_ge {X: Type} {f: nat -> X} {n x m} : n <= m -> Nat.iter n (scons x) f m = f (m - n).
proof: Proof. move=> ?. have {1}->: m = n + (m - n) by lia. by rewrite iter_scons. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun