proposition: Lemma in_lift_subst : forall Q G i, In (Some Q) (lift_subst G i) -> (exists2 W, In (Some W) G & Q = lift W i).
proof: Proof. induction G. simpl; tauto. intros i Q_G. unfold lift_subst_comp in Q_G; simpl in Q_G. destruct Q_G. destruct a; try discr. exists t. auto with datatypes. unfold lift_subst_comp in H; simpl in H. congruence. destruct (IHG i); trivial. exists x; auto with datatypes. Qed.
imports: Coq(Compare_dec Arith Lia) CoLoR(RelExtras ListExtras LogicUtil)