gistfile1.txt

Section TMP.
    Variable A : Set.
    Variables a b : A.

    Definition f (n : nat) : A :=
        match n with
        | 0 => a
        | _ => b
        end.

    Goal (exists f : nat -> A, f 0 = a /\ f 1 = b).
    exists f; auto.
    Qed.
End TMP.