+lemma loop_S_true :
+ ∀A,n,f,p,a. p a = true →
+ loop A (S n) f p a = Some ? a.
+#A #n #f #p #a #pa normalize >pa //
+qed.
+
+lemma loop_S_false :
+ ∀A,n,f,p,a. p a = false →
+ loop A (S n) f p a = loop A n f p (f a).
+normalize #A #n #f #p #a #Hpa >Hpa %
+qed.
+