proposition: Lemma subst_dom_singleton G T : isSingletonSubst T G -> exists E, subst_dom G = Some (type T) :: E /\ emptyEnv E.
proof: Proof. intro. inversion H. destruct G; try_solve. destruct o; try_solve. exists (subst_dom G); split. inversion H0; trivial. apply subst_dom_Empty. intro p; apply (H1 p). Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)