proposition: Lemma subst_ran_lifted_ne : forall G, ~isEmptySubst G -> subst_ran (lift_subst G 1) = None :: subst_ran G.
proof: Proof. induction G; intro GR_nn. absurd (isEmptySubst nil); trivial. apply subst_nil_empty. simpl; unfold lift_subst_comp. destruct a. rewrite !subst_ran_cons_some, lift_env. destruct (subst_empty_dec G) as [Ge | G_ne]. rewrite subst_ran_lifted_empty; trivial. rewrite subst_ran_empty; trivial. rewrite !env_sum_empty_r. unfold liftedEnv; simpl. unfold finalSeg; simpl. rewrite initialSeg_full; solve [auto with datatypes | lia]. rewrite IHG; trivial. simpl. unfold finalSeg; simpl. rewrite initialSeg_full; solve [auto with datatypes | lia]. rewrite !subst_ran_cons_none. apply IHG. intro Ge. absurd (isEmptySubst (None::G)); trivial. apply subst_cons_empty; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)