-theorem track_inv_impi: \forall P,p,q,r,S. Track P (impi p q r) S \to
- \exists Q,A,B,D,i. \exists a,b:Formula.
- S = pair (impl a b) D \land
- Track P p (pair A a) \land
- Track P q (pair b B) \land
- Track Q r (pair lleaf D) \land
- Insert (pair A B) i P Q.
- intros; inversion H; clear H; intros; subst; autobatch depth = 12 width = 5 size = 16.
+theorem ntrack_inv_impi: \forall P,p,q,r,S. NTrack P (impi p q r) S \to
+ \exists Q,A,B,D,i. \exists a,b:Formula.
+ S = pair (impl a b) D \land
+ NTrack P p (pair A a) \land
+ NTrack P q (pair b B) \land
+ NTrack Q r (pair lleaf D) \land
+ Insert (pair A B) i P Q.
+ intros; inversion H; clear H; intros; destruct; autobatch depth = 12 width = 5 size = 16.