Variables p q : Type. Variable F : p -> p. Variable X : p. (* Lambda is "fun" and the dot is "=>" *) (* Definition I := fun x => x. *) Definition I : p -> p := fun x => x. Check I. Print I. Check I X. Eval compute in I X. Definition K : p -> q -> p := fun x y => x. (* Definition K := fun (x:p) (y: q) => x. *) Check K. Definition Dwa: (p->p)-> p->p := fun f x => f( f x). Check Dwa. Definition Cztery : (p->p)-> p->p := fun f x => f(f(f( f x))). Check fun f x => Dwa(Dwa f)x. Eval compute in Dwa (Dwa F) X. Eval compute in Dwa (Dwa F). Eval compute in Cztery F X. Eval compute in (Dwa (Dwa F) X = Cztery F X). Check (Dwa (Dwa F) X = Cztery F X). Eval compute in X = X. Lemma tosamo: (Dwa (Dwa F) X = Cztery F X). reflexivity. Qed. Check tosamo. Print tosamo.