proposition: Lemma leftmost_poly_var_many_poly_abs {n t x} : leftmost_poly_var (many_poly_abs n t) = Some x <-> leftmost_poly_var t = Some (n+x).
proof: Proof. elim: n x; first done. move=> n /= IH x. have ->: S (n + x) = n + S x by lia. rewrite -IH. case: (leftmost_poly_var (many_poly_abs n t)); last done. move=> [|y]; first done. constructor; by move=> [->]. Qed.
imports: List Lia Relation_Definitions Relation_Operators Operators_Properties Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts iipc2_facts pure_typing_facts) ssreflect ssrbool ssrfun