Dep_nonsense.v

Require Import List Utf8 Vector Fin Psatz.
Import Notations ListNotations.

Require Import Lia
  Coq.Unicode.Utf8
  Coq.Bool.Bool
  Coq.Init.Byte
  Coq.NArith.NArith
  Coq.Strings.Byte
  Coq.ZArith.ZArith
  Coq.Lists.List.

Open Scope N_scope.

(* a more complicated definition, for no reason, that I wrote before the simple one *)
Definition np_total (np : N):  (np <? 256 = true) ->  byte.
Proof.
  intros H.
  refine(match (np <? 256) as b return ∀ mp, np = mp ->
      (mp <? 256) = b -> _ with
   | true => fun mp Hmp Hmpt =>
      match of_N mp as npt return _ = npt -> _ with
      | Some x => fun _ => x
      | None => fun Hf => _
      end eq_refl
   | false => fun mp Hmp Hmf => _
  end np eq_refl eq_refl).
  abstract(
  apply of_N_None_iff in Hf;
  apply N.ltb_lt in Hmpt; nia).
  abstract (subst; congruence).
Defined.

(* Now I am trying to prove the same theorem again *)
Lemma np_true : forall np (Ha : np <? 256 = true) x,
  of_N np = Some x -> np_total np Ha = x.
Proof.
  intros * Hb; unfold np_total.
  (* Goal: I want to rewrite Ha but it appears in
    in the term np_total_tmp_subproof0 np Ha mp Hmp Hmf
    so generalize it
  *)
  generalize (np_total_subproof0 np Ha) as f.
  generalize (eq_refl (np <? 256)).
  set (u := np <? 256) in *.
  unfold u at 1. 
  rewrite Ha; subst u. 
  intros * f.
  generalize (np_total_subproof np np eq_refl e).
  rewrite Hb; intros;
  reflexivity.
Qed.