proposition: Lemma subst_conv_cons G G' Q : G ~~(Q) G' -> None :: (lift_subst G 1) ~~(envSubst_lift1 Q) None :: (lift_subst G' 1).
proof: Proof. intros. constructor; intros. destruct x; destruct y; try_solve. destruct Q; try_solve. inversion H1. destruct (var_subst_lift_rev G 1 H3) as [W [GxW TW]]. assert (envSub Q x y). destruct Q; try_solve. destruct (sc_lr H y H2 GxW) as [W' [G'yW' WW']]. exists (lift W' 1); split. apply var_subst_cons. apply var_subst_lift; trivial. rewrite TW. apply terms_conv_conv_lift; trivial. destruct x; destruct y; try_solve. destruct Q; try_solve. inversion H1. destruct (var_subst_lift_rev G' 1 H3) as [W [GxW TW]]. assert (envSub Q x y). destruct Q; try_solve. destruct (sc_rl H x H2 GxW) as [W' [G'yW' WW']]. exists (lift W' 1); split. apply var_subst_cons. apply var_subst_lift; trivial. rewrite TW. apply terms_conv_conv_lift; trivial. destruct x; try_solve. inversion H0. destruct (var_subst_lift_rev G 1 H2) as [W [GxW _]]. destruct (sc_inj_l H GxW). exists (S x0). destruct Q; try_solve. destruct y; try_solve. inversion H0. destruct (var_subst_lift_rev G' 1 H2) as [W [GxW _]]. destruct (sc_inj_r H GxW). exists (S x). destruct Q; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)