proposition: Lemma term_size_pos (P: term) : term_size P = S (term_size P - 1).
proof: Proof. case: P => /= *; by lia. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts) ssreflect ssrbool ssrfun