A beginner's question:

```
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 ? *)
```

why would it be?

Is it that you want something like `inversion`

, `dependent destruction`

, or `dependent elimination`

(from Equations)?

lengyijun has marked this topic as resolved.

@James Wood Thx

Last updated: Jan 28 2023 at 06:30 UTC