Refinement of a Jordan-Hölder series of a group $G$ Let $G$ be a group with identity element $e$. 
A sequence $(K_i)_{0\leq i\leq n}$ of subgroups of $G$ is called a composition series of the group $G$ if  


*

*$K_{i+1}\lhd K_i$, for all $0\leq i\leq n-1$;

*$K_0=G$ and $K_n=\{e\}$.


A composition series $(K_i)_{0\leq i\leq n}$ of $G$ is called a Jordan-Hölder series if


*

*$(K_i)_{0\leq i\leq n}$ is strictly decreasing;

*There exists no strictly decreasing proper refinement of $(K_i)_{0\leq i\leq n}$.


Ok—now, let $(K_i)_{0\leq i\leq n}$ be a Jordan-Hölder series of the group $G$. Suppose $(H_j)_{0\leq j\leq m}$ is a composition series of $G$ which refines $(K_i)_{0\leq i\leq n}$ and is distinct from $(K_i)_{0\leq i\leq n}$. How can I formally prove that $(H_j)_{0\leq j\leq m}$ must be derived from $(K_i)_{0\leq i\leq n}$ by repeating certain terms?
 A: I won’t give you a formal proof${}^{1}$, but here is one that includes a lot of the details explicitly.
Your nomenclature is nonstandard. What you call a “composition series” is usually called a subnormal series. What you call a “Jordan-Holder series” is normally called a composition series. I will use the standard nomenclature.
Lemma 1. Let $S$ be a simple group. If
$$1 = H_n\triangleleft H_{n-1}\triangleleft H_{n-2}\triangleleft\cdots \triangleleft H_0 = S$$
is a subnormal series, then there exists $i$, $0\lt i\lt n$, such that $H_0=H_1=\ldots=H_{i-1}=S$ and $H_{i}=H_{i+1}=\cdots=H_n = \{e\}$. 
Proof. Let $i$ be the smallest index such that $H_{i}\neq S$; thus, $H_{0}=\cdots=H_{i-1}=S$. Since $H_{i}\triangleleft H_{i-1}=S$, $S$ is simple, and $H_i\neq S$, then $H_i=\{e\}$; since $\{e\}=H_n\subseteq \cdots \subseteq H_i=\{e\}$, we have $H_n=\cdots = H_i=\{e\}$, as claimed. $\Box$
Lemma 2. Let $\{e\}=H_n\triangleleft H_{n-1}\triangleleft\cdots \triangleleft H_0=G$ be a composition series; that is, a strictly ascending subnormal series that does not admit a strictly ascending refinement. Then for each $i$, $0\leq i \leq n-1$, $H_i/H_{i+1}$ is simple.
Proof. Fix $i$; since the series is strictly ascending, then $H_i/H_{i+1}$ is nontrivial. Let $K$ be a normal subgroup of $H_i/H_{i+1}$. Then there exists a (unique) subgroup $N$ of $H_i$ corresponding to $K$; that is, $H_{i+1}\subseteq N$ and $N/H_{i+1} = K$. By the correspondence theorem, $N\triangleleft H_i$, and since $H_{i+1}\triangleleft H_i$, then $H_{i+1}\triangleleft N$. Thus, inserting $N$ between $H_{i+1}$ and $H_i$ yields a refinement of the composition series; therefore, $N=H_{i+1}$ or $N=H_i$; hence either $K=H_{i+1}/H_{i+1}$ or $K=H_i/H_{i+1}$. That is: a normal subgroup of $H_{i+1}/H_i$ is either trivial or the whole group. Hence, $H_{i+1}/H_i$ is simple. $\Box$
Now suppose that $1=K_n\triangleleft K_{n-1}\triangleleft \cdots \triangleleft K_0=G$ is a composition series; suppose that you have a refinement of this series given by subgroups $(H_j)$. Fix $i$, and say $K_{i+1}=H_{s+t}\triangleleft H_{s+t-1}\triangleleft \cdots \triangleleft H_{s}=K_{i}$. 
Then $1 =\frac{H_{s+t}}{H_{s+t}} \triangleleft \frac{H_{s+t-1}}{H_{s+t}} \triangleleft \cdots \triangleleft \frac{H_s}{H_{s+t}} = \frac{K_i}{K_{i+1}}$ is a subnormal series for $\frac{K_i}{K_{i+1}}$, which by Lemma 2 is simple. (Note that $H_{s+t}=K_{i+1}$ is normal in $K_i=H_s$, hence normal in each of the $H_j$, $s\leq j\leq s+t$, so all those quotients make sense). Thus, by Lemma 1, there is a $j$ such that $1=\frac{H_{s+t}}{H_{s+t}} = \cdots = \frac{H_{s+t-j+1}}{H_{s+t}}$ and $\frac{H_{s+t-j}}{H_{s+t}} = \cdots = \frac{H_{s}}{H_{s+t}}=\frac{K_i}{K_{i+1}}$. By the correspondence theorem, this means that $K_{i+1}=H_{s+t}=\cdots = H_{s+t-j+1}$ and $H_{s+t-j}=\cdots = H_s=K_i$. So the terms between $K_{i+1}$ and $K_i$ are just repeats of $K_{i+1}$ and $K_i$.
As this holds for each $i$, we conclude that the refinement of the original composition series consisted of adding repeated terms interpolating each the $K_i$.

${}^1$ To quote the great philosopher I. Montoya I do not think that means what you think it means. A formal proof of proposition $P$ in the theory $\Gamma$ is a finite sequence $(s_0,\ldots,s_n)$ such that:


*

*For each $i$, $s_i$ is a well-formed formula (WFF) in the language of $\Gamma$;

*$s_n=P$; and

*For each $i$, $s_i$ is either:
(a) An axiom of $\Gamma$; or
(b) A tautology; or
(c) The result of applying a valid rule of inference of $\Gamma$ to a subset of the initial segment $(s_0,\ldots,s_{i-1})$.


Since you did not specify a theory $\Gamma$, I suspect you don’t actually want a formal proof.
