| track_impw: \forall P,r,D,a,b. Track P r (pair lleaf D) \to
Track P (impw r) (pair (impl a b) D)
| track_impr: \forall P,r. \forall a,b:Formula.
Track P r (pair a b) \to
Track P (impr r) (pair lleaf (impl a b))
| track_impw: \forall P,r,D,a,b. Track P r (pair lleaf D) \to
Track P (impw r) (pair (impl a b) D)
| track_impr: \forall P,r. \forall a,b:Formula.
Track P r (pair a b) \to
Track P (impr r) (pair lleaf (impl a b))