-let corec at_ext: āf1,f2. šā¦f1ā¦ ā šā¦f2ā¦ ā
- (āi,i1,i2. @ā¦i, f1ā¦ ā” i1 ā @ā¦i, f2ā¦ ā” i2 ā i1 = i2) ā f1 ā f2 ā ?.
+lemma istot_tl: āf. šā¦fā¦ ā šā¦ā«±fā¦.
+#f cases (pn_split f) *
+#g * -f /2 width=3 by istot_inv_next, istot_inv_push/
+qed.
+
+(* Properties on tls ********************************************************)
+
+lemma istot_tls: ān,f. šā¦fā¦ ā šā¦ā«±*[n]fā¦.
+#n elim n -n /3 width=1 by istot_tl/
+qed.
+
+(* Main forward lemmas on at ************************************************)
+
+corec theorem at_ext: āf1,f2. šā¦f1ā¦ ā šā¦f2ā¦ ā
+ (āi,i1,i2. @ā¦i, f1ā¦ ā” i1 ā @ā¦i, f2ā¦ ā” i2 ā i1 = i2) ā
+ f1 ā f2.