proposition: Lemma leftmost_poly_var_ren_poly_type {ξ t} : leftmost_poly_var (ren_poly_type ξ t) = omap ξ (leftmost_poly_var t).
proof: Proof. elim: t ξ; [done | by move=> ? + ? _ ? /= => -> |]. move=> t + ? /= => ->. case: (leftmost_poly_var t); [by case | done]. 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