An example of a proof with a function.

Definition contrapositive :
  forall P : Prop,
  forall Q : Prop,
  (~Q -> ~P) -> P -> Q 
:= 
fun 
  (P : Prop) 
  (Q : Prop) 
  (H : ~Q -> ~P) 
  (p : P) => 
  let nnq : ~ ~ Q := (fun (e : ~Q) => H e p) in 
  let H' :  ~ ~ Q -> Q := NNPP Q in 
  (H' nnq) 
.