proposition: Lemma subst_ran_singleton G T : isSingletonSubst T G -> subst_ran G = env T.
proof: Proof. intro. inversion H. destruct G; try_solve. destruct o; try_solve. rewrite subst_ran_cons_some. rewrite subst_ran_empty. autorewrite with terms. inversion H0; try_solve. intro p; apply (H1 p). Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)