How to derive the formula for line correspondences to estimate a homography? When calculating a homography with line correspondences instead of point correspondences, what is the derivation of the formula:
$$
l_i = H^T\cdot l^{'}_i
$$
I know that:
$$
l^T\cdot x = 0 \quad\text{and}\quad l^{'T}\cdot x^{'} = 0\\
\text{with}\quad x^{'} = H\cdot x\\
\text{then}\quad l^{'T}\cdot H\cdot x = 0
$$
But I don't know how to continue.
 A: You are almost there. Now, just note that your result
$$0=l'^THx=(H^Tl')^Tx$$
should hold for all points on the line $l$ in the first image. As a consequence, it follows that $l\sim H^Tl'$, as desired.
A: I will provide a complete proof.
Assumptions


*

*$\mathbf{l}^T \mathbf{x} = 0$, for all 2d points $\mathbf{x} \in \mathbb{R}^3$ represented in homogenous coordinates that belong to $\mathbf{l}^T \in \mathbb{R}^3$ (i.e. a homogenous representation of a line, in a plane).

*Similarly, $\mathbf{l}'^T \mathbf{x}' = 0$, for all points $\mathbf{x}' \in \mathbb{R}^3$ that lie on the other line $\mathbf{l}' \in \mathbb{R}^3$ (i.e. a homogenous representation of a line, in another plane).

*$\mathbf{x}' = \mathbf{H} \mathbf{x}$, for some homography $\mathbf{H} \in \mathbb{R}^{3 \times 3}$.


Theorem
We want to prove that $\mathbf{l} = \mathbf{H}^T \mathbf{l}'.$
Proof
We can combine 3 with 2 to obtain
\begin{align}
\mathbf{l}'^T \mathbf{x}' &= 0 \iff \\
\mathbf{l}'^T \left(\mathbf{H} \mathbf{x} \right)&= 0
\end{align}
Given that matrix multiplication is associative, we don't need the parentheses
\begin{align}
\mathbf{l}'^T \mathbf{H} \mathbf{x} = 0 \label{1}\tag{1}
\end{align}
Now, note that $\mathbf{l}'^T \mathbf{H} = (\mathbf{H}^T \mathbf{l}')^T$, then \ref{1} becomes 
\begin{align}
(\mathbf{H}^T \mathbf{l}')^T \mathbf{x} = 0
\end{align}
Now, we know that $\mathbf{l}^T \mathbf{x} = 0$, so
\begin{align}
(\mathbf{H}^T \mathbf{l}')^T \mathbf{x} &= \mathbf{l}^T \mathbf{x} \iff \\
(\mathbf{H}^T \mathbf{l}')^T &= \mathbf{l}^T \iff \\
\mathbf{H}^T \mathbf{l}' &= \mathbf{l}
\end{align}
Note that this equality holds up to scale (because we are working in projective space).
