Print.v

(* This is with Set Printing All *)

Error: Abstracting over the term "np <? 256" leads to a term
λ b : bool,
  ∀ f : ∀ mp : N, np = mp → (mp <? 256) = false → byte,
    (if b as b0 return (∀ mp : N, np = mp → (mp <? 256) = b0 → byte)
     then
      λ (mp : N) (Hmp : np = mp) (Hmpt : (mp <? 256) = true),
        match of_N mp as npt return (of_N mp = npt → byte) with
        | Some x0 => λ _ : of_N mp = Some x0, x0
        | None => λ Hf : of_N mp = None, np_total_subproof np mp Hmp Hmpt Hf
        end eq_refl
     else λ (mp : N) (Hmp : np = mp) (Hmf : (mp <? 256) = false), f mp Hmp Hmf)
      np eq_refl eq_refl = x
which is ill-typed.


Reason is: Illegal application: 
The term
 "if b as b return (∀ mp : N, np = mp → (mp <? 256) = b → byte)
  then
   λ (mp : N) (Hmp : np = mp) (Hmpt : (mp <? 256) = true),
     match of_N mp as npt return (of_N mp = npt → byte) with
     | Some x => λ _ : of_N mp = Some x, x
     | None => λ Hf : of_N mp = None, np_total_subproof np mp Hmp Hmpt Hf
     end eq_refl
  else λ (mp : N) (Hmp : np = mp) (Hmf : (mp <? 256) = false), f mp Hmp Hmf"
of type "∀ mp : N, np = mp → (mp <? 256) = b → byte"
cannot be applied to the terms
 "np" : "N"
 "eq_refl" : "np = np"
 "eq_refl" : "b = b"
The 3rd term has type "b = b" which should be coercible to 
"(np <? 256) = b".


(* This one without Set Printing All *)

Error: Abstracting over the term "np <? 256" leads to a term
λ b : bool,
  ∀ f : ∀ mp : N, np = mp → (mp <? 256) = false → byte,
    (if b as b0 return (∀ mp : N, np = mp → (mp <? 256) = b0 → byte)
     then
      λ (mp : N) (Hmp : np = mp) (Hmpt : (mp <? 256) = true),
        match of_N mp as npt return (of_N mp = npt → byte) with
        | Some x0 => λ _ : of_N mp = Some x0, x0
        | None => λ Hf : of_N mp = None, np_total_subproof np mp Hmp Hmpt Hf
        end eq_refl
     else λ (mp : N) (Hmp : np = mp) (Hmf : (mp <? 256) = false), f mp Hmp Hmf)
      np eq_refl eq_refl = x
which is ill-typed.
Reason is: Illegal application: 
The term
 "if b as b return (∀ mp : N, np = mp → (mp <? 256) = b → byte)
  then
   λ (mp : N) (Hmp : np = mp) (Hmpt : (mp <? 256) = true),
     match of_N mp as npt return (of_N mp = npt → byte) with
     | Some x => λ _ : of_N mp = Some x, x
     | None => λ Hf : of_N mp = None, np_total_subproof np mp Hmp Hmpt Hf
     end eq_refl
  else λ (mp : N) (Hmp : np = mp) (Hmf : (mp <? 256) = false), f mp Hmp Hmf"
of type "∀ mp : N, np = mp → (mp <? 256) = b → byte"
cannot be applied to the terms
 "np" : "N"
 "eq_refl" : "np = np"
 "eq_refl" : "b = b"
The 3rd term has type "b = b" which should be coercible to 
"(np <? 256) = b".