-lemma loop_S_true :
- ∀A,n,f,p,a. p a = true →
- loop A (S n) f p a = Some ? a. /2/
-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.
-
-lemma trans_init_sep: