qed.
theorem track_inv_impw: \forall P,p,S. Track P (impw p) S \to
\exists B,a,b.
S = pair (impl a b) B \land
Track P p (pair lleaf B).
qed.
theorem track_inv_impw: \forall P,p,S. Track P (impw p) S \to
\exists B,a,b.
S = pair (impl a b) B \land
Track P p (pair lleaf B).