proposition: Lemma subst_conv_singleton M G G' Q : Q.(envSub) 0 0 -> isSingletonSubst M G -> G ~~(Q) G' -> exists M', isSingletonSubst M' G' /\ M ~(Q) M'.
proof: Proof. intros. destruct H0. destruct (sc_lr H1 0 H H0) as [W [NW MW]]. exists W; split; trivial. constructor; trivial. intro i. destruct (nth_error_In G' (S i)) as [[T GT] | Gn]; auto. destruct T. destruct (sc_inj_r H1 GT). destruct x. absurd (0 = S i). lia. apply envSub_Lok with Q 0; trivial. apply conv_subst_udecl with G Q (S x); trivial. constructor 2; trivial. constructor; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)