Check bool. Check true. Check Prop. Check True. Section propositions. Variables a b : Prop. Check (~ a -> False /\ b). End propositions. Section bool. Variables a b : bool. Check (andb (implb (negb a) false) b). End bool. Check nat. Check nat -> nat -> bool. Check (fun f x => f (f x)). Check (fun A f (x:A) => f (f x)). Check (fun x => (x + 3)). Check (forall x, x=x). Check (forall x : nat, x=x). Check (forall A (x : A), x=x). Check (forall A, (exists x : A, x=x)). Eval compute in (False /\ True). Eval compute in (false && true)%bool. Eval compute in (false || true)%bool. Eval compute in (implb false true). Definition double A f := fun x : A => f (f x). Eval compute in (double _ (fun x => x + 3) 3). Require Import List. Check list. Check nil. Check (nil : list nat). Check 1::2::nil.