proposition: Lemma eq_variable_dec : forall v1 v2 : var, {v1 = v2} + {v1 <> v2}.
proof: Proof. intros; decide equality. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List