proposition: Lemma var_subst_cons G x T : G |-> x / T -> (None :: G) |-> (S x) / T.
proof: Proof. intro GxT. unfold varSubstTo in *; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)