proposition: Lemma subst_dom_Empty : forall G, isEmptySubst G -> emptyEnv (subst_dom G).
proof: Proof. induction G. simpl; intro; apply emptyEnv_empty. intro aG_empty. destruct a. absurd ((Some t :: G) |-> 0 /- ); trivial. intro w; destruct w; try_solve. intro p; destruct p. right; try_solve. unfold VarUD; simpl. apply IHG. apply subst_tail_empty; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)