-theorem at_inv_monotonic: ∀t,i1,j1. @⦃i1, t⦄ ≡ j1 → ∀i2,j2. @⦃i2, t⦄ ≡ j2 → j2 < j1 → i2 < i1.
-#t #i1 #j1 #H elim H -t -i1 -j1
-[ #t #i2 #j2 #_ #H elim (lt_le_false … H) //
-| #t #i1 #j1 #_ #IH #i2 #j2 #H #Hj elim (at_inv_xOx … H) -H *
+theorem at_inv_monotonic: ∀t1,i1,j1. @⦃i1, t1⦄ ≡ j1 → ∀t2,i2,j2. @⦃i2, t2⦄ ≡ j2 → t1 ≐ t2 → j2 < j1 → i2 < i1.
+#t1 #i1 #j1 #H elim H -t1 -i1 -j1
+[ #t1 #t2 #i2 #j2 #_ #_ #H elim (lt_le_false … H) //
+| #t1 #i1 #j1 #_ #IH * #b2 #t2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht
+ #H0 #Ht destruct elim (at_inv_xOx … H) -H *