- loop A k1 f p a1 = Some ? a2 → f a2 = a3 →
- loop A k2 f q a3 = Some ? a4 →
- loop A (k1+k2) f q a1 = Some ? a4.
+ loop A k1 f p a1 = Some ? a2 →
+ f a2 = a3 → q a2 = false →
+ loop A k2 f q a3 = Some ? a4 →
+ loop A (k1+k2) f q a1 = Some ? a4.
+#Sig #f #p #q #Hpq #k1 elim k1
+ [normalize #k2 #a1 #a2 #a3 #a4 #H destruct
+ |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?);
+ cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
+ [#eqa1a2 destruct #eqa2a3 #Hqa2 #H
+ whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr
+ whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H
+ |normalize >(Hpq … pa1) normalize
+ #H1 #H2 #H3 @(Hind … H2) //
+ ]
+ ]
+qed.