Section vl25. Variable A:Set. Variable B:A->Prop. Check (forall(x:A),B x). Check ex. Check (ex (A:=A) B). Print ex. Print ex_intro. Check nat. Print nat. Check 0. Print nat_ind. Require Import List. Print List. Print list. Print list_ind. Check nat_rec. Print nat_rec. Print nat_rect. Check nat_ind. Check list. (* Check nil. *) Check (nil (A:=A)). Inductive vector (A:Set) : nat -> Set := | Vnil : vector A 0 | Vcons : forall (a:A) (n:nat), vector A n -> vector A (S n). Print nat_rec. Section bla. Variable m:nat. Definition f (n:nat) := nat_rec (fun _ => nat) m (fun n' => fun r => S r) n. Eval simpl in f 0. Eval simpl in f 1. Eval simpl in (fun n => f (S n)). End bla. Print f. Eval simpl in f 3 4. Eval simpl in f 4 11. Check list. Check nil (A:=nat). Check cons 2 nil. Print list. Set Implicit Arguments. Inductive tree (A: Set) : Set := | leaf : tree A | node : A -> tree A -> tree A -> tree A. Check tree_ind. Check leaf. Check node. Implicit Arguments node [A]. Implicit Arguments leaf [A]. Print tree.