Definition negb (b:bool) := match b with | true => false | false => true end. Definition andb (b1 b2:bool) := match b1,b2 with | true, true => true | _,_ => false end. Print andb. (*andb = fun b1 b2 : bool => if b1 then if b2 then true else false else false : bool -> bool -> bool *) (* (fun x => negb (andb false x)) --> (fun x => negb false) --> (fun x => true) (fun x => negb (andb x false)) --> (fun x => if if x then if false then true else false else false then false else true)--> (fun x => if if x then false else false then true else false) no more reduction possible *) Fixpoint prodn (A:Type) n : Type := match n with | 0 => unit | 1 => A | S k => (A * prodn A k)%type end. Fixpoint length {A:Type} (l:list A) : nat := match l with | nil => 0 | cons _ l' => S (length l') end. Fixpoint embed {A} (l:list A) : prodn A (length l) := match l return prodn A (length l) with | nil => tt | cons a l' => let p' : prodn A (length l') := embed l' in let h : prodn A (length l') -> prodn A (length (a::l')) := match l' with | nil => fun _:unit => a | cons a' l'' => fun p':prodn A (length(a'::l'')) => (a,p') end in h p' end.