proposition: Lemma subst_dom_varNotSubst : forall G x, G |-> x/- -> subst_dom G |= x :!.
proof: Proof. induction G. destruct x; unfold VarUD; auto with datatypes. intros x xUD. destruct x. unfold varIsNotSubst in xUD; simpl in *. destruct a. destruct xUD; discr. unfold VarUD; auto. unfold VarUD; simpl. apply IHG; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)