Consultas de Práctico

Buenas, tengo unas pequeñas dudas de estos ejercicios. En el ej2 al definir Xor me aparece el siguiente error: Error: The constructor false (in type bool) expects no arguments.

Esto pasa al poner dos false en al match. Lo tengo definido de la siguiente forma:

Definition Xor (b1 b2 : bool) :=
                              match b1 b2 with
                                | false false => false
                                | true true => false
                                | true false => true
                              end.

La otra duda es sobre la función LeBool del ej3. No me queda claro si está bien definido de esta forma ya que estoy aplicando recursión en las dos variables:

Fixpoint leBool (n m:nat):bool :=
                                match n with
                                  | 0 => match m with
                                          | 0 => false
                                          | S k => true
                                         end
                                  | S k => match m with
                                            | 0 => false
                                            | S t => leBool k t
                                           end
                                end.

Gracias.