Here are two well known "classic" functions over polymorphic lists.
map f l
computes a new list from l
by applying f
to each of its elements.
let rec map (f : 'a > 'b) : 'a list > 'b list = function
 [] > []
 h :: t > f h :: map f t
;;
mem x l
returns true
is x
is an element of l
and returns false
if it
is not.
let rec mem (a : 'a) : 'a list > bool = function
 [] > false
 x :: l > a = x  mem a l
;;
If y
is an element of the list obtained by
mapping f
over l
then there must be an
element x
in l
such that
f x = y
. Conversely, if there exists an x
in l
such that y = f x
,
then y
must be a member of the list obtained by
mapping f
over l
.
We attempt a proof of correctness of the given definitions with respect to this property.
Lemmamem_map_iff
:
∀ (f : α → β) (l : α list) (y : β),
mem y (map f l) ⇔ ∃(x : α), f x = y ∧ mem x l.
Proof: We first treat the forward implication
∀ (f : α → β) (l : α list) (y : β), mem y (map f l) ⇒ ∃(x : α), f x = y ∧ mem x l
l
.
l = []
: Show
mem y (map f []) ⇒ ∃(x : α), f x = y ∧ mem x []
. mem y (map f []) ≡ False
. Proof follows (ex falso quodlibet).
 Show
l
has formx' :: l
(usel
now to refer to the tail): Assume the induction hypothesis:
mem y (map f l) ⇒ ∃x, f x = y ∧ mem x l
.
 We are required to show for an arbitrary
(x' : α)
:mem y (map f (x' :: l)) ⇒ ∃(x : α), f x = y ∧ mem x (x' :: l)
.
 By simplification, we can rewrite the above to:
f x' = y ∨ mem y (map f l) ⇒ ∃(x : α), f x = y ∧ (x' = x ∨ mem x l).
 We assume then an
(x' : α)
and a(y : β)
such that:f x' = y ∨ mem y (map f l)
.mem y (map f l) ⇒ ∃(x : α), f x = y ∧ mem x l
.
 Show
∃(x : α), f x = y ∧ (x' = x ∨ mem x l)
: First consider
f x' = y
in (1). Take
x = x'
in the goal.  Then by (1)
f x = y ∧ x = x'
.  So
x'
is a witness.
 Take
 Now consider
mem y (map f l)
in (1).∃(x^{*} : α), f x^{*} = y ∧ mem x^{*} l
by (2). Take
x = x^{*}
in the goal.  By the above
f x^{*} = y ∧ mem x^{*} l
 So
x^{*}
is a witness.
 First consider
 Assume the induction hypothesis:

We now work on the reverse implication. We want to show that
and proceed by induction on∀ (f : α → β) (l : α list) (y : β), ∃(x : α), f x = y ∧ mem x l ⇒ mem y (map f l)
l
.
l = []
: Assume
x
,y
withf x = y ∧ mem x []
.  Show
mem y (map f [])
: mem x [] ≡ false
. Proof follows (ex falso quodlibet).
 Assume
l
has formx' :: l
(usel
now to refer to the tail): Assume the induction hypothesis:
∃(x : α), f x = y ∧ mem x l ⇒ mem y (map f l)
.
 We are required to show for an arbitrary
(x' : α)
:∃ (x : α), f x = y ∧ mem x (x' :: l) ⇒ mem y (map f (x' :: l))
 By simplification, we can rewrite the above to:
∃ (x : α), f x = y ∧ x = x' ∨ mem x l ⇒ f x' = y ∨ mem y (map f l)
.
 Assume the goal and induction hypotheses:
 There is
(x : α)
and(y : β)
such that:f x = y ∧ (x = x' ∨ mem x l)
f x = y ∧ mem x l ⇒ mem y (map f l)
 There is
 Show
f x' = y ∨ mem y (map f l)
: Assume
x = x'
in (1) and showf x' = y
: Since,
f x = y
is given by (1.),f x' = y
.
 Since,
 Assume
mem x l
in (1) and showmem y (map f l)
: Rewrite
mem y (map f l)
via (2) tof x = y ∧ mem x l
. f x = y
by (1) somem y (map f l)
.
 Rewrite
 Assume
 Assume the induction hypothesis:
References:
"Sofware Foundations"  Pierce et. al.