proposition: Lemma subst_dom_singleton_after_none_decl : forall i T, subst_dom (copy i None ++ {x/T}) |= i := type T.
proof: Proof. induction i. simpl; constructor. trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)