fact: Definition find_in_ctx {var : Type} (term : nat) (ctx : @var_context.var_context var) : M (option var) := (mfix1 find_in_ctx (ctx : @var_context.var_context var) : M (option var) := (mmatch ctx with | [? v xs] (var_context.cons term v xs) =n> M.ret (Some v) | [? x v xs] (var_context.cons x v xs) =n> find_in_ctx xs | _ => M.ret None end)) ctx.
imports: Coq.ZArith.ZArith Coq.Lists.List