- Track Q r (pair lleaf D) \to
- Insert (pair A B) i P Q \to
- Track P (impi p q r) (pair (impl a b) D)
+ Track (abst P p q (pair A B)) r (pair lleaf D) \to
+ Track P (impi p q r) (pair (impl a b) D)
+ | track_scut: \forall P,p,q,A,B. \forall c:Formula.
+ Track P p (pair A c) \to
+ Track P q (pair c B) \to
+ Track P (scut p q) (pair A B)