-nlet rec list_ind (A:Type) (P:list A → Prop) (p:P (nil A)) (f:(Πa:A.Πl':list A.P l' → P (cons A a l'))) (l:list A) on l ≝
- match l with [ nil ⇒ p | cons h t ⇒ f h t (list_ind A P p f t) ].
-
-nlet rec list_rec (A:Type) (P:list A → Set) (p:P (nil A)) (f:Πa:A.Πl':list A.P l' → P (cons A a l')) (l:list A) on l ≝
- match l with [ nil ⇒ p | cons h t ⇒ f h t (list_rec A P p f t) ].
-
-nlet rec list_rect (A:Type) (P:list A → Type) (p:P (nil A)) (f:Πa:A.Πl':list A.P l' → P (cons A a l')) (l:list A) on l ≝
- match l with [ nil ⇒ p | cons h t ⇒ f h t (list_rect A P p f t) ].
-