proposition: Lemma iter_scons_lt {X: Type} {x: X} {f: nat -> X} {n m: nat} : m < n -> Nat.iter n (scons x) f m = x.
proof: Proof. elim: n m f; first by lia. move=> n IH [|m] f /= ?; first done. by rewrite /funcomp IH; first by lia. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun