proposition: Lemma subst_dom_singleton_after_none_nodecl : forall i j T, i <> j -> subst_dom (copy i None ++ {x/T}) |= j :! .
proof: Proof. induction i; intros. destruct j; simpl. lia. constructor; destruct j; trivial. destruct j. constructor 2; trivial. simpl; trivial. destruct (IHi j T); try_solve. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)