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