proposition: Lemma highest_var_list_descr (x:list h10upc) (h:h10upc) : In h x -> highest_var h <= highest_var_list x.
proof: Proof. induction x as [|hh x IH]. - intros []. - intros [hhh|hx]. + cbn. rewrite hhh. lia. + cbn. specialize (IH hx). lia. Qed.
imports: Arith Lia List Undecidability.DiophantineConstraints(H10C)