Require Import
  Coq.Lists.List
  PeanoNat
  Lia.

Inductive u8 : Set :=
  | u8_cons : nat -> u8.

Inductive immut_u8_bw : Set :=
  | immut_u8_bw_cons : nat -> immut_u8_bw.


Inductive origin : Set :=
  | origin_cons : nat -> origin.


Inductive mir : Set :=
  | borrow_immut (x : immut_u8_bw) (y : u8).

Inductive mark_as_loan_origin : list mir -> origin -> Prop :=
  | borrow_immut_mark_as_loan_origin : forall l i (x : immut_u8_bw)(y : u8),
                                       Some(borrow_immut x y) = nth_error l i
                                    -> mark_as_loan_origin l (origin_cons (length l + i)).


Lemma loan_larger_length : forall l o,
                           mark_as_loan_origin l (origin_cons o)
                        -> o >= length l.
Proof.
intros.
generalize H; intros.
destruct H.
(* stuck here *)
(* Why o is not substituted in the goal ? *)