proposition: Lemma subst_dom_varSubst : forall G x T, G |-> x/T -> subst_dom G |= x := type T.
proof: Proof. induction G. destruct x; try_solve. intros x T Gx. destruct x. destruct a. inversion Gx; try_solve. try_solve. unfold VarD; simpl. apply IHG; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)