proposition: Lemma var_subst M G (MG: correct_subst M G) : isVar M -> { T:Term & { x:nat | G |-> x/T & term (subst MG) = term T }} + { term (subst MG) = term M }.
proof: Proof. intro. term_inv M. autorewrite with terms. unfold presubst; simpl. destruct (varSubst_dec G x) as [[W Gx] | Gxn]. left; exists W; exists x; trivial. rewrite Gx; rewrite lift_0; trivial. right. destruct Gxn; rewrite H0; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)