## Stream: Coq users

### Topic: ✔ Why variable is not substituted?

#### lengyijun (Aug 02 2022 at 13:07):

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?

#### James Wood (Aug 03 2022 at 08:43):

Is it that you want something like `inversion`, `dependent destruction`, or `dependent elimination` (from Equations)?

#### Notification Bot (Aug 03 2022 at 11:30):

lengyijun has marked this topic as resolved.

#### lengyijun (Aug 03 2022 at 11:31):

@James Wood Thx

Last updated: Jun 14 2024 at 18:01 UTC