proposition: Lemma varSubst_dec G x : {T: Term | G |-> x/T} + { G |-> x/- }.
proof: Proof. destruct (nth_error_In G x) as [[T Gx] | Gnx]. destruct T as [T |]. left; exists T; auto. right; auto with terms. right; auto with terms. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)