proposition: Lemma iter_up_ren_iter_up_ren {n ξ1 ξ2 x} : Nat.iter n up_ren ξ1 (Nat.iter n up_ren ξ2 x) = Nat.iter n up_ren (ξ2 >> ξ1) x.
proof: Proof. have [?|->] : x < n \/ x = n + (x - n) by lia. - rewrite [Nat.iter _ _ ξ2 x]iter_up_ren_lt; first done. rewrite iter_up_ren_lt; first done. by rewrite iter_up_ren_lt; first done. - by rewrite ?iter_up_ren /funcomp. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.Facts ssreflect ssrbool ssrfun