Module RegionAccess

Set Implicit Arguments.
Require Import DeBruijn.
Require Import MyTactics.
Require Import Types.
Require Import Programs.
Require Import ValueLists.
Require Import Typing.
Require Import Environments.
Require Import Multiplicity.
Require Import MultiplicityEnvironments.
Require Import Canonical.
Require Import PreliminaryLemmas.
Require Import Resources.
Require Import ResourcesContinued.
Require Import InversionClassification.

-------------------------------------------------------------------------

The inhabitants of a region are well-typed. These lemmas are typically used when we have both an inhabitant, of type TyAt _, and a capability for the region, of type TyRegionCap _ _ _.

Lemma ji_inversion:
  forall R vs T,
  ji R vs T ->
  forall v,
  member v vs ->
  jv R nil nil v T.

Proof.

unfold member. induction 1; simpl. tauto. intros ? [ ? | ? ]; subst;
eauto using j_value_resource_weakening, (@star_commutative resource).
Qed.