proposition: Lemma subst_ran_single T : subst_ran {x/T} = env T.
proof: Proof. unfold subst_ran; simpl. destruct (env T); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)