proposition: Lemma conv_subst_udecl G G' Q x y : G ~~(Q) G' -> Q.(envSub) x y -> G |-> x/- -> G' |-> y/- .
proof: Proof. intros. destruct (nth_error_In G' y) as [[T GT] | Gn]; auto. destruct T. destruct (sc_rl H x H0 GT) as [W [GW _]]. inversion H1; inversion GW; try_solve. constructor 2; trivial. constructor; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)