proposition: Lemma subst_type_comp M G x T : correct_subst M G -> G |-> x/T -> env M |= x := type T \/ env M |= x :!.
proof: Proof. intros MG Gx. destruct MG. inversion Gx. destruct (isVarDecl_dec (env M) x) as [[A MxA] | MxN]. left. rewrite (dom_c0 x (type T) A); trivial. apply subst_dom_varSubst; trivial. auto. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)