proposition: Lemma subst_ran_single_after_empty T : forall i, subst_ran (copy i None ++ {x/T}) = env T.
proof: Proof. induction i. simpl; apply subst_ran_single. unfold subst_ran; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)